Questions tagged [proof-theory]
Questions about analysis of proofs in theories
57
questions
6
votes
0
answers
173
views
Could a quantum computer prove theorems with infeasibly long proofs?
The mathematician Andrew Granville recently published a
"philosophical" article, Accepted proofs: Objective truth, or culturally robust?.
At the end, he mentions in passing a suggestion by ...
- 7,465
3
votes
1
answer
185
views
How far is the distance between Mahlo Universe and Mahlo Cardinal?
There seems to be some literature stating that Mahlo Universe[1][2] is the counterpart of Mahlo Cardinal in type theory, but I don't fully understand this point of knowledge.
More explicitly, I would ...
- 151
1
vote
0
answers
149
views
What is the model of computation that corresponds (in the manner of Curry-Howard) to the deduction rule of resolution?
The Curry-Howard Correspondence is well-documented for the isomorphism which associates the intuitionistic natural deduction proof calculus (logic side) with the type system for the simply typed ...
- 81
4
votes
1
answer
135
views
Is there a relation between the techniques used by Dan Willard, versus those of Brown and Palsberg, to exclude diagonalization?
This question extends my inquiry from a previous post [0].
Dan Willard's Self-Justifying Axiom Systems/Self-Verifying Theories [1] and Brown and Palsberg's self-interpreter for F-Omega [2] both employ ...
- 81
2
votes
0
answers
94
views
Is there a relationship between Brown and Palsberg's Self-Interpreter for F-Omega and Lawvere's Fixed Point Theorem?
Brown and Palsberg [0] demonstrated an self-interpreter for F-Omega. To do so, they perform "a careful analysis of the classical theorem [of the impossibility of self-interpretation by total ...
- 81
6
votes
0
answers
94
views
Relationship between natural deduction refutation and tableaux for propositional logic
Which kind of relationship is there between natural deduction refutations of a set f propositional logic assumptions, and the corresponding tableaux?
For example, consider the unsatisfiable set $\...
- 1,588
0
votes
0
answers
195
views
Confusion about different definitions of LK, LJ, NK, and NJ
I try to understand the differences between the calculi mentioned above, mainly the difference between natural deduction and the sequence calculus. For this I consulted the wikipedia article on the ...
- 11
2
votes
0
answers
122
views
Asymptotic complexity lower bounds of proof checking
This paper on universal search mentions (on pp. 6-7) that proof checking can be done in $O(n^2)$ where $n$ is the length of the proof. Is this optimal? I don't want to specify the problem too ...
- 153
0
votes
1
answer
143
views
What is a known sequence for which being constant is not provable?
My question concerns the property of being constant for computable functions ${\mathbb N}\to \{0,1\}$, within any common framework $T$ strong enough to include Heyting arithmetic (and of course not ...
- 505
4
votes
3
answers
415
views
Proving proof system properties within the proof system itself?
While reading about Frege proof systems in [1], I came across the completeness theorem and its proof, which involves a few lemmas introduced first. Here are the first two of those lemmas:
$$\begin{...
user30584
1
vote
0
answers
253
views
Is there a standard definition of resolution for arbitrary clauses?
Knuth defines in [1] a resolution operator for arbitrary clauses which sets $C = C' \diamond C'' = (C' \lor C'')$ when there is no literal $x$ such that $x \in C'$ and $\neg x \in C''$. I skimmed over ...
user30584
4
votes
0
answers
95
views
Relative consistency of various Martin-Löf style type theories
I am wondering about relative consistency of various Martin-Löf type theories, when compared to one another, I will use MLTT for the intensional Martin-Löf type theory with $\Pi$, $\Sigma$, $\mathbb{N}...
- 900
17
votes
2
answers
2k
views
Proof relevance vs. proof irrelevance
I want to use use Agda to help me write proofs, but I am getting contradictory feedback about the value of proof relevance.
Jacques Carette wrote a Proof-relevant Category Theory in Agda library. But ...
- 575
0
votes
2
answers
266
views
Why is plus-comm a b $:\equiv$ refl (plus a b) not a proof of the commutativity of addition?
I've been curious about the 'geometric situation' that one has when considering the type
$\prod_{(n,m:\textrm{Nat})}(\textrm{plus}\ n\ m) = (\textrm{plus}\ m\ n)$.
Here, addition is defined in the ...
5
votes
1
answer
159
views
Does focused proof search ever have to backtrack across the choice of focus formula?
There are a lot of different "focused" sequent calculi for lots of different logics, but my understanding is that many or most of them have the following flavor. First one divides the ...
- 675
6
votes
1
answer
156
views
What arithmetical theorems can plain $\lambda \Pi$ reason about?
I've read that System F cannot state or prove theorems of the First Order Theory of Arithmetic. I assume this is because we lack dependent types, so we cannot explicitly express $\forall n:\mathbb{N}....
- 219
3
votes
2
answers
129
views
Understanding non-equivalence of proof lengths according to proof systems
Here, in section 4.3, Fortnow says:
But to prove P != NP we would need to show that tautologies
cannot have short proofs in an arbitrary proof system.
I am ...
4
votes
1
answer
219
views
The theory of definitions in first order logic
I'm looking for a clear and thorough treatment of the theory of definitions in first order predicate logic from a syntactic/proof theoretic point of view (as opposed to semantic/model theoretic point ...
- 354
9
votes
2
answers
754
views
How do continuations represent negations (under the Curry–Howard correspondence)?
Under the Curry–Howard correspondence, types can be thought of as propositions, and values inhabiting a type can be thought of as proofs that the corresponding proposition is true. (E.g., the ...
- 193
8
votes
0
answers
617
views
An axiom for John Major's Equality
In the the standard library of Coq, there is the axiom:
Axiom JMeq_eq : forall (A:Type) (x y:A), JMeq x y -> x = y.
Why isn't it provable? Can it be reduced ...
- 381
3
votes
0
answers
65
views
Efficient transformation of clausal proof into resolution proof
Clausal proof is used to certify unsat results of SAT solvers. However the main theoretical results are on resolution proof (for instance, the non existence of a polynomial resolution proof for the ...
- 311
6
votes
1
answer
222
views
Resolution vs Nondeterministic Search Problems
It is well known that each resolution refutation $\Pi$ for an unsatisfiable CNF formula $F = C_1\wedge C_2 \wedge ... \wedge C_m$ over variables $X$ can be translated in polynomial time (in the size ...
- 1,062
1
vote
1
answer
299
views
Practical approaches to solving whether programs will halt
What kinds of systems are available that accept a certain program $P$ and attempts to figure out "the program does terminate" or "the program does not terminate" and output a proof of one or the other?...
- 1,641
6
votes
2
answers
1k
views
Efficiently modeling Turing machines in Peano Arithmetic
The (undecidable) Peano Arithmetic (PA) is powerful enough to model Turing machines.
Consider a standard first order axiomatization of Peano Arithmetic and a standard Hilbert-style proof system $\...
- 22.6k
13
votes
0
answers
268
views
Categorical semantics for S5 modal logic?
Does anyone know where I can look to find out what the generally categorical semantics of S5 is?
For S4, the answer is well-known: we want a Cartesian closed category with a product-preserving ...
- 32.4k
3
votes
0
answers
143
views
What is the largest complexity class that a non-Turing complete proof assitant, like Coq, can achieve? [duplicate]
Given that all functions in Coq will terminate, it cannot cover the entire $RE$. So what is the class it can achieve? Is it $R$?
8
votes
1
answer
165
views
What is the proof-theoretic significance of the existence of a Brown-Palsberg self-interpreter for system $F_\omega$?
In A Self-Interpreter for F-omega, Brown and Palsberg construct for each term of each type $x:T$ a representation $\bar x : \Box T$ (a metatheoretical function which can't be represented in the ...
- 343
16
votes
1
answer
746
views
Relative consistency of PA and some type theories
For a type theory, by consistency, I mean that it has a type which is not inhabited. From the strong normalization of the lambda cube, it follows that system $F$ and system $F_\omega$ are consistent. ...
- 343
4
votes
1
answer
158
views
Is there any work relating type systems and Cook-Reckhow proof systems?
An important subfield of computational complexity is proof complexity, mostly due to Cook and Reckhow. E.g. one notable result is that a proof system that has efficient proofs (i.e., in length ...
- 175
9
votes
1
answer
676
views
Why is Proof Checker required in Proof Carrying Code
In the classical PLDI'98 paper by Necula, "The design and implementation of a certifying compiler", the high-level verifier uses:
VCGen to generate verification conditions (safety predicates)
First-...
- 193
-1
votes
1
answer
167
views
Undecidable Single Programs [closed]
So the halting problem basically states that there cannot exist any finite length algorithm for automatically verifying if other finite length algorithms terminate.
But suppose I start listing out ...
- 369
16
votes
3
answers
1k
views
Why do constructivists not seem to care too much about call/cc
So a little while back I first had someone tell me that call/cc could allow proof objects for classical proofs by implementing Peirce's law. I did some thinking about the topic recently and I can't ...
- 1,141
3
votes
2
answers
515
views
About the position of side conditions in an inference rule
Sometimes I see people put side conditions above the inference line as if they were premises of an inference rule. This feels strange. My understanding (which may be wrong) is that a side condition ...
- 2,775
8
votes
1
answer
144
views
Hypersequents: proof term assigments or translations to hybrid logic
I've been looking at a modal logic with the axiom
$$
(\Diamond A \land \Diamond B) \to \Diamond((A \land \Diamond B) \vee (A \land B) \vee (A \land \Diamond B))
$$
Roughly, this says that the ...
- 32.4k
9
votes
2
answers
1k
views
Turing machines whose termination is unprovable?
I have a naive question: does there exist a Turing machine whose termination is true but unprovable by any natural, consistent and finitely axiomatizable theory? I ask for a mere existence proof ...
- 314
7
votes
2
answers
336
views
SAT in some DTIME always via a constructive proof?
Why can the statement $SAT \in DTIME(n^3)$ not be proven through a non-constructive proof? Intuitively a proof would be a turing machine, which solves this problem in $DTIME(n^3)$, but there are non-...
- 81
3
votes
2
answers
482
views
Derivation of cut rule in sequent calculus
I searched internet but could not find any good weblink which shows how the cut rule for sequent calculus can be derived.
I found this paper but it uses implication elimination rule which I cannot ...
- 133
1
vote
2
answers
161
views
Is there an $\mathcal{L}$-theory and a formula $\phi$ for which Kolmogorov(proof($\phi$)) $<$ Kolmogorov($\phi$)?
Are there a complete decidable $\mathcal{L}$-theory, a formula $\phi$ and a proof of $\phi$ for which the Kolmogorov complexity of the proof of $\phi$ is less than the Kolmogorov complexity of $\phi$?
...
- 113
18
votes
3
answers
1k
views
funsplit and polarity of Pi-types
In a recent thread on the Agda mailing list, the
question of $\eta$ laws popped up, in which Peter Hancock made thought-provoking remark.
My understanding is that $\eta$ laws come with negative
...
- 478
17
votes
2
answers
4k
views
Is propositional resolution a complete proof system?
This question is about propositional logic and all occurrences of "resolution" should be read as "propositional resolution".
This question is something extremely basic but it has been bothering me ...
- 12.6k
4
votes
1
answer
983
views
Why is there a need for cyclic proofs?
I was reading a paper A Generic Cyclic Theorem Prover. This paper explains about automated theorem prover based on various instantiations like the notion of first order logic equations with inductive ...
- 143
10
votes
1
answer
322
views
Unification-based elimination rule for equality
A few years back, I ran across the following left-rule for equality in sequent calculus:
$$
\frac{s \doteq t \leadsto \theta \qquad
\theta(\Gamma) \vdash \theta(C)}
{\Gamma, s \doteq t ...
- 32.4k
5
votes
1
answer
284
views
Resolution vs Extended Resolution
Let $R(f)$ and $ER(f)$ be the minimum-size for unsat proofs of $f$ in Resolution and Extended Resolution respectively. What's the best bound we have on $D=\min_f (R(f)-ER(f))$ where $f$ belongs to a ...
- 51
12
votes
1
answer
460
views
Barendregt's proof of subject reduction for $\lambda2$
I found a problem in Barendregt's proof of subject reduction (Thm 4.2.5 of Lambda calculi with types).
The last step of the proof (page 60), says:
"and hence by Lemma 4.1.19(1), $\quad\Gamma,x:\rho\...
- 701
16
votes
3
answers
1k
views
Can we prove weak normalization for System F by induction on a transfinite ordinal
Weak normalization for the simple typed lambda calculus can be proved (Turing) by induction on $\omega^2$. An extended lambda calculus with recursors on natural numbers (Gentzen) has a weak ...
user6892
6
votes
1
answer
190
views
converse relationship between the cut rule and the identity axiom
On page 30 of "Proofs and Types" by Girard, Taylor, and Lafont, it is claimed that that the identity axiom for sequent calculus:
C ├ C
has a converse relation with the cut rule:
$$\frac{\vec{A} \...
- 323
29
votes
1
answer
976
views
Inductive types for large countable ordinal notations.
I'm looking to build notations for large countable ordinals in a "natural way". By "natural way" I mean that given an inductive data type X, that equality should be the usual recursive equality (the ...
- 618
11
votes
2
answers
349
views
References to programming languages based on conditional logics
Conditional logics are logics which augment traditional logical implication with modal operators corresponding to other notions of condition (for example, the causal conditional $A\; \square\!\!\!\!\...
- 32.4k
15
votes
1
answer
381
views
Looking for papers and articles on the Tarskian Möglichkeit
Some background: Łukasiewicz many-valued logics were intended as modal logics, and Łukasiewicz gave an extensional definition of the modal operator:
$\Diamond A =_{def} \neg A \to A$ (which he ...
- 815
26
votes
1
answer
1k
views
Are types propositions? (What are types exactly?)
I've been reading a lot on type systems and such and I understand roughly why they were introduced (in order to resolve Russel's paradox). I also understand roughly their practical relevance in ...
- 677