20

The short answer to your question 1 is no, but for perhaps subtle reasons. First of all, System $F$ and $F_\omega$ cannot express the first-order theory of arithmetic, and even less the consistency of $\mathrm{PA}$. Secondly, and this is really surprising, $\mathrm{PA}$ can actually prove consistency of both those systems! This is done using the so-called ...


19

The purpose of the proof checker is to minimise the trusted computing base. By having a proof checker, neither the compiler nor the theorem prover need to be correct. The paper makes this point on Page 3: Neither the compiler nor the prover need to be correct in order to be guaranteed to detect incorrect compiler output. This is a significant advantage ...


19

Constructive mathematics is not just a formal system but rather an understanding of what mathematics is about. Or to put it differently, not every kind of semantics is accepted by a constructive mathematician. To a constructive mathematician call/cc looks like cheating. Consider how we witness $p \lor \lnot p$ using call/cc: We provide a function $f$ which ...


16

There are several possible notions of proof relevance. Let us consider three similar situations: An element of a sum $\Sigma (x : A) . P(x)$ is a pair $(a, p)$ where $a : A$ and $p$ is a proof of $P(a)$. An element of $\Sigma (x : A) . \|P(x)\|$, where $\|{-}\|$ is propositional truncation, is a pair $(a, q)$ where $a : A$ and $q$ is an equivalence class ...


13

I recommend that everyone first read Andrej Bauer's answer, as he covers all the basics extremely well. I agree with everything he says in his answer. I humbly offer more comments, even though I know less on this topic than he does - but I was mentioned by name, as was my project. When I gave a talk about agda-categories, I explained one thing about it that ...


10

As you note, there is a possible constructive interpretation of classical logic in this sense. The fact that classical logic is equiconsistent with intuitionistic logic (say, Heyting Arithmetic) has been known for quite some time (already in 1933, e.g. Godel) using a double negation translation. By a more sophisticated argument, it can be shown that Peano ...


9

Termination of a Turing machine (on a fixed input) is a $\Sigma^0_1$ sentence and all usual first-order arithmetic theories are complete for $\Sigma^0_1$ sentences, i.e. all true $\Sigma^0_1$ statements are provable in these theories. If you look at totality in place of halting, i.e. a TM halts on all inputs, then that is a $\Pi^0_2$-complete sentence and ...


8

I would like to elaborate on Kaveh's answer because I see people wondering about the constructive status of $P = NP$. Levin's algorithm performs a dove-tailing parallel execution of all Turing machines on the given SAT instance. If and when any machine terminates, it is verified whether its output is a solution to the SAT instance. If so, Levin's algorithm ...


8

There is no proof significance, since already Gödel's $T$ has a Brown-Palsberg self-interpreter for free. We need a better definition of a typed self-interpreter.


8

I agree with both Andrej's and Cody's answer. However, I think it is also worth mentioning why constructivists should care about control operators (call/cc). These operators are usually connected to classical logic because when people looked at their typing rules (Felleisen, Griffin) they noticed that the types have the form of Peirce's Law or double-...


7

When one associates negation with continuations, it is probably not ideal to think of it in terms of an 'empty' type. Continuation passing can be done with respect to any result type, and if that type is held abstract, it works a lot like 'false' in that there is no introduction rule for it. With respect to the paper you linked (I'm by no means an expert on ...


6

Cook-Reckhow propositional proof systems are nonunifrom. E.g. the computational complexity counterpart to the class of polynomial-size $\mathsf{Extended Frege}$ proofs is the nonuniform complexity class $\mathsf{P/poly}$. We have to look at their uniform counterparts: E.g. the proof complexity counterpart for $\mathsf{P}$ are bounded arithmetic theories ...


6

It is not entirely clear what you mean by a nonconstructive proof of P=NP. I am guessing that you are asking if it is possible to prove that there is a polynomial time algorithm for SAT without providing one. That cannot be the case because we can prove that Levin's universal search algorithm for SAT has optimal running time, if P=NP is true (even if it is ...


6

I don't have the books handy at the moment, but I think Shoenfield's "Mathematical Logic" and Hinman's "Fundamentals of Mathemtical Logic" would contain much if not all of what you're looking for. Probably not what you want but perhaps worth mentioning anyway is A. P. Morse's book "A Theory of Sets". This is a development of (a rather idiosyncratic version ...


6

Let $T$ be a reasonble theory of arithmetic, say $\mathrm{PA}$. Consider the sequence $$f(m) = \begin{cases} 1 & \text{if $m$ encodes a proof of $\vdash_T 0 = 1$} \\ 0 & \text{otherwise} \end{cases} $$ The sequence is clearly computable, even primitive recursive and therefore representable in $T$. If there is $m$ such that $f(m) = 1$ then $T$ is ...


5

As Andrej notes, $\lambda\Pi$ is a conservative extension of first-order logic which means: Adding the axioms of PA to $\lambda\Pi$ gives exactly the same arithmetic theorems as PA. However, because of the more expressive system, it is possible to finitely axiomatize induction using the following (encoding of) this axiom: $$ \forall P: {\mathbb N}\...


4

The fact that a system is complete for proving valid formulas without the cut rule doesn't mean you can derive the cut rule from other rules. In fact it is not difficult to construct counter-examples. Consider $\Rightarrow A \rightarrow B$ and $\Rightarrow A$. From these assumptions it would follow that $\Rightarrow B$. But you cannot derive it without ...


4

The current Software Foundations book does explain all this later on: https://softwarefoundations.cis.upenn.edu/lf-current/ProofObjects.html So if you're following the book, just read on :)


4

Yes, an example of a system that performs this task is T2. It does not solve the halting problem but instead it only attempts to solve certain special cases. A overview is at https://en.wikipedia.org/wiki/Microsoft_Terminator . The newest version of this system is at https://mmjb.github.io/T2/ .


4

But it does follow. The types $$A = \prod_{(n,m:\textrm{Nat})}(\textrm{plus}\ n\ m) = (\textrm{plus}\ n\ m)$$ and $$B = \prod_{(n,m:\textrm{Nat})}(\textrm{plus}\ n\ m) = (\textrm{plus}\ m\ n)$$ are both contractible. Indeed, they are both inhabited and because $\mathrm{Nat}$ is a set, its identity type is a proposition, hence so are $A$ and $B$, as they are ...


3

Addressing the question in the title: $\mathsf{\lambda n\,m.\,refl}$ is not a proof of commutativity by definition because addition is not a constant function by definition. Of course, the commutativity proof can be shown to be propositionally equal (by a "dependent" equality, or path-over-path) to the $\mathsf{refl}$-returning one, by Andrej's ...


3

Yes, backtracking in focused proof search may be necessary due to a wrong choice of focus formula. Consider the provable sequent $$\vdash p\otimes q, (p^\bot\mathrel{\wp} q^\bot)\otimes r, r^\bot.$$ Choosing to focus on $p\otimes q$ leads to a dead end, because however you "split" the context you end up with an atom ($p$ or $q$) without matching ...


3

A little consideration about point 3. "Is it true that every "human written proof" that is expressible in ZFC has indeed an "efficient" representation in ZFC?" It turns out that the question is anything but new. At least it dates back to the late sixties when the idea of computer vierified mathematical proofs came up (e.g. Automath): In his 'A survey of ...


3

I am not sure I understand the question, specially the informal part. If by it you mean essentially how we generally argue for correctness of things, I woke interpret it as day proofs in ZFC or something like that. In any case we can express provability of a statement in a computably axiomatizable system in PA (and in fact in weaker systems). Now you are ...


3

I know this is a bit late, but perhaps it is still of interest. While not exactly the logic you are interested in, Gödel-Dummett logic, the intermediate logic characterised by linear Kripke-frames, is closely related to S4.3, and for this logic people have looked into similar questions: The paper A Lambda Calculus for Goedel-Dummett Logic Capturing ...


3

I'm not a logic expert, but I believe the answer is no. If the Turing machine halts, and the system is strong enough, you ought to be able to write out the full computation history of the Turing machine on its input. When one verifies that the result of the computation is a terminating sequence of transitions, one can see that the machine halts. ...


3

There is no loop. The purpose of a formal system is to make reasoning principles explicit and to explain more precisely how reasoning works. The word "foundation" in "foundations of mathematics" does not mean "create a secure base for mathematics out of nothing" – that would be an indifensible position. There is absolutely ...


3

The first problem is what does is even mean that a propositional proof system can prove its own properties: there is a serious discrepancy of the languages, because the propositional proof system can only express propositional formulas, whereas properties of the proof system are first-order statements in a language that can reason about finite strings, i.e., ...


2

Showing that from two cut-free derivations $\Gamma \vdash A$ and $\Gamma, A \vdash C$ you can produce a cut-free derivation of $\Gamma \vdash C$ is called cut admissibility. Admissibility of cut is actually equivalent to showing that cut can be eliminated. If you have cut-elimination, you just cut the two derivations together and then eliminate the cut. On ...


2

An inference rule is a symbolic representation of an entire family of closure rules. A side condition cuts down such a family to a subfamily. It is perhaps best to show an example. We consider the following toy variant of the propositional calculus. The language of expressions is built from primitive constants $\top$ and $\bot$, and a binary connective $\...


Only top voted, non community-wiki answers of a minimum length are eligible