21
votes
Accepted
Proof relevance vs. proof irrelevance
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(...
- 28.3k
20
votes
Accepted
Relative consistency of PA and some type theories
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 ...
- 13.7k
14
votes
Proof relevance vs. proof irrelevance
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 ...
- 1,530
9
votes
Accepted
How do continuations represent negations (under the Curry–Howard correspondence)?
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 ...
- 921
8
votes
What is the proof-theoretic significance of the existence of a Brown-Palsberg self-interpreter for system $F_\omega$?
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.
- 28.3k
6
votes
Accepted
What is a known sequence for which being constant is not provable?
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{...
- 28.3k
6
votes
Accepted
Is there any work relating type systems and Cook-Reckhow proof systems?
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 ...
- 21.5k
6
votes
The theory of definitions in first order logic
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.
...
- 161
5
votes
Accepted
What arithmetical theorems can plain $\lambda \Pi$ reason about?
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, ...
- 13.7k
4
votes
Accepted
Is there a relation between the techniques used by Dan Willard, versus those of Brown and Palsberg, to exclude diagonalization?
I'll defer if someone more knowledgeable on the subject arrives, but I think the answer is that they are not the same.
Willard's work is about building theories that avoid the typical formulation of ...
- 921
4
votes
Accepted
Why is plus-comm a b $:\equiv$ refl (plus a b) not a proof of the commutativity of addition?
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 ...
- 28.3k
4
votes
Accepted
Practical approaches to solving whether programs will halt
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/...
- 1,641
4
votes
How would I go about learning the underlying theory of the Coq proof assistant?
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 :)
- 141
3
votes
About the position of side conditions in an inference rule
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 ...
- 28.3k
3
votes
Efficiently modeling Turing machines in Peano Arithmetic
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 ...
- 22.6k
3
votes
Accepted
Efficiently modeling Turing machines in Peano Arithmetic
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 ...
- 21.5k
3
votes
Why is plus-comm a b $:\equiv$ refl (plus a b) not a proof of the commutativity of addition?
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 ...
- 1,444
3
votes
Accepted
Does focused proof search ever have to backtrack across the choice of focus formula?
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.$$
...
- 5,273
2
votes
Accepted
Understanding non-equivalence of proof lengths according to proof systems
I believe everything you said is correct. I note that your point #3 could hold regardless of points #1 and #2 - points #1 and #2 are just a concrete example of where this has provably happened.
- 36.9k
2
votes
Accepted
How far is the distance between Mahlo Universe and Mahlo Cardinal?
It's awkward to ask yourself questions, but...
Rathjen, M. (2003). Realizing Mahlo set theory in type theory. Archive for Mathematical Logic, 42(1), 89-101.
The chapter 5, "Realizing set theory ...
- 151
2
votes
Accepted
Proving proof system properties within the proof system itself?
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 ...
- 16.9k
2
votes
Proving proof system properties within the proof system itself?
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 ...
- 28.3k
1
vote
Proving proof system properties within the proof system itself?
In general, proof systems can sometimes prove some of their properties within themselves.
A nice example of this is the fact that NL=Co-NL can be proved "within NL".
This video might also be ...
- 1,596
1
vote
Understanding non-equivalence of proof lengths according to proof systems
A propositional proof system in which all tautologies have a "short" proof is called a super-propositional-proof system. Such a system exists iff NP = CoNP.
If NP != CoNP then P != NP.
So, it's not ...
- 111
1
vote
Resolution vs Nondeterministic Search Problems
If I understood correctly the question, the so-called Buss-Pudlak game provides a simple transformation from a proof system to such a decision tree (see Buss-Pudlak '94 http://math.cas.cz/%7Epudlak/...
- 1,899
Only top scored, non community-wiki answers of a minimum length are eligible