2022 Developer Survey is open! Take survey.
20 votes
Accepted

Why do constructivists not seem to care too much about call/cc

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 ...
user avatar
  • 26.4k
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 ...
user avatar
  • 13.1k
19 votes
Accepted

Why is Proof Checker required in Proof Carrying Code

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 ...
user avatar
17 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(...
user avatar
  • 26.4k
13 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 ...
user avatar
11 votes

Why do constructivists not seem to care too much about call/cc

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 ...
user avatar
  • 13.1k
9 votes

Why do constructivists not seem to care too much about call/cc

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 ...
user avatar
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.
user avatar
  • 26.4k
8 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 ...
user avatar
  • 566
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. ...
user avatar
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 ...
user avatar
  • 21.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{...
user avatar
  • 26.4k
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, ...
user avatar
  • 13.1k
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 :)
user avatar
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/...
user avatar
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 ...
user avatar
  • 26.4k
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 ...
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.$$ ...
user avatar
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 ...
user avatar
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 ...
user avatar
  • 21.3k
3 votes
Accepted

Hypersequents: proof term assigments or translations to hybrid logic

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, ...
user avatar
  • 146
2 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 ...
user avatar
  • 26.4k
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.
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 ...
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 ...
user avatar
  • 26.4k
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 ...
user avatar
  • 1,456
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 ...
user avatar
  • 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/...
user avatar
1 vote
Accepted

Undecidable Single Programs

One way to look at your question is the Busy Beaver Numbers. What we will do is restrict a Turing Machine so that: The blank symbol is a $0$ The tape alphabet is $\{0, 1\}$ The input to our turing ...
user avatar
  • 1,102

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