Skip to main content
Share Your Experience: Take the 2024 Developer Survey
23 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(...
Andrej Bauer's user avatar
  • 29.1k
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 ...
cody's user avatar
  • 13.9k
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 ...
Jacques Carette's user avatar
11 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 ...
Dan Doel's user avatar
  • 1,021
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.
Andrej Bauer's user avatar
  • 29.1k
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{...
Andrej Bauer's user avatar
  • 29.1k
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 ...
Kaveh's user avatar
  • 21.7k
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. ...
Andreas Blass's user avatar
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, ...
cody's user avatar
  • 13.9k
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 ...
Dan Doel's user avatar
  • 1,021
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 ...
Andrej Bauer's user avatar
  • 29.1k
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/...
Joshua Herman's user avatar
4 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 ...
Marzio De Biasi's user avatar
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 :)
Catalin Hritcu's user avatar
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 ...
Andrej Bauer's user avatar
  • 29.1k
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 ...
Kaveh's user avatar
  • 21.7k
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 ...
András Kovács's user avatar
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.$$ ...
Damiano Mazza's user avatar
3 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 ...
Ember Edison's user avatar
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.
Joshua Grochow's user avatar
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 ...
Emil Jeřábek's user avatar
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 ...
Andrej Bauer's user avatar
  • 29.1k
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 ...
Avi Tal's user avatar
  • 1,606
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 ...
Parry's user avatar
  • 111
1 vote

How do continuations represent negations (under the Curry–Howard correspondence)?

Actually, your question is too narrowly-focused. For intuitionist logic, and its underlying Heyting lattice, for any formula $X$, the subset of formulae $\overline{A} = A → X$ is a reverse-mapping of ...
NinjaDarth's user avatar
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/...
Iddo Tzameret's user avatar

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