Questions tagged [proof-theory]
Proof theory is an area of logic that studies proof as formal mathematical objects. If you'd like advice on the presentation of a proof you have in draft, use proof-writing instead. If you'd like feedback on its validity, use proof-verification. If none of the above apply, you do not need a proof-* tag.
907
questions
3
votes
1
answer
73
views
Natural Deduction: An unusual(?) presentation
1. Context
On page 241 of their paper Natural deduction and coherence for weakly distributive categories Blute et al give the right- and left-introduction rules of multiplicative conjunction for (...
- 1,707
2
votes
0
answers
60
views
Proofs and Types: Girard's remarks on Theoretical Computing
In the first chapter of Girard's Proofs and Types (1989) one finds the following remarks:
Theoretical Computing is not yet a science. Many basic concepts have not been clarified, and current work in ...
- 1,707
25
votes
5
answers
2k
views
Are there are any inherent mathematical reasons some proofs are difficult?
This is not a complaint about my proofs course being difficult, or how I can learn to prove things better, as all other questions of this flavour on Google seem to be. I am asking in a purely ...
- 466
1
vote
0
answers
83
views
Is consistency with the $\omega$-rule absolute to $\omega$-models?
According to Wikipedia, a theory $T$ that interprets arithmetic is consistent with the $\omega$-rule if and only if it has an $\omega$-model. That would mean that consistency with the $\omega$-rule is ...
- 763
1
vote
1
answer
111
views
Why Hilbert's 24th Problem is unsolvable?
Hilbert's famous 24th problems handles the problem of the simplest possible proof of a mathematical statement, in a nutshell.
It is said that there are a few problems with this problem. First of all, ...
- 59
0
votes
0
answers
15
views
Conservativity and proof-theoretical ordinals
I assume the second-order arithmetical theory $T$ in concern is consistent and r.e.
The most well-known kind of proof-theoretical ordinal $\|T\|$ of $T$ is the $\Pi_1^1$-ordinal, defined as
$\|T\|=\{$...
- 11
1
vote
0
answers
21
views
Formulas that can be proved from the uniform reflection schema
Let $T$ be a sound, r.e. theory containing elementary arithmetic. By the uniform reflection schema of $T$ ($\mathrm{RFN}(T)$) I mean the schema that expresses the soundness of $T$:
$\forall x(\...
- 11
1
vote
0
answers
17
views
Strength and conservativity of $\Sigma^1_n \textrm{-DC}_0$
How strong is $\Sigma^1_n \textrm{-DC}_0$ in terms of consistency strength? I know it is conservative to $\Pi^1_n \textrm{-TI}_0$, but I don't know its relation to other subsystems. Are there any ...
- 233
2
votes
0
answers
88
views
In the context of Morse–Kelley set theory how does truth compare to satisfaction in an unbounded class of $V_\kappa$s?
I've been studying Vopenka's principle:
For any language $\mathcal{L}$ and a proper class $C$ of $\mathcal{L}$-structures, there exist distinct $M, N \in C$ and an elementary embedding $j: M \to N$.
...
- 233
2
votes
1
answer
138
views
Is there a distinction between rules of inference and axioms in Homotopy Type Theory (HoTT)?
I'm taking rules of inference to be metalinguistic and to describe when you can write down a certain syntactic expression in the object-language given that you already have others written down (e.g. &...
- 89
0
votes
1
answer
47
views
Is it possible to use order relation in Presburger arithmetic?
The signature of Presburger arithmetic contains only the addition
operation and equality, omitting the multiplication operation
entirely.
Is it possible to state and prove theorems in Presburger ...
- 387
1
vote
1
answer
41
views
Can Peano arithmetic be completed using only atomic $\omega$-completions?
Say we have an axiomatizable theory $T$ extending $Th(A_E)$ where $A_E$ are the axioms of arithmetic. What I call an atomic $\omega$-completion of $T$ (I am not sure if there is a more standard ...
- 58.7k
0
votes
0
answers
52
views
Are logical rules logics?
When I asked whether the empty logic (the one on which no argument is valid) is axiomatizable, the consensus was that it is, and that it is axiomatized by a proof system having no rules whatsoever.
Is ...
0
votes
1
answer
58
views
Prove that $\mathbf{L}$ is almost a normal modal logic.
Suppose we have a logic $\mathbf{L}$ containing all the propositional tautologies and the formula $\square(p\wedge q)\leftrightarrow(\square p \wedge\square q)$, and it is closed by Modus Ponens, ...
- 815
2
votes
0
answers
50
views
Is the empty logic axiomatizable?
Obviously this is a bit of an edge case. By the empty logic I mean the one on which all arguments are invalid, i.e. $\Gamma \nvdash \varphi$ for all sets of formulas (premises) $\Gamma$ and any ...
3
votes
0
answers
193
views
Which sentences are irreducibly self-referential?
Below, all sentences/formulas are in the language of arithmetic, and for simplicity we conflate numbers with numerals and sentences with Godel numbers.
Now asked at MO.
Say that a sentence $\varphi$ ...
- 218k
2
votes
0
answers
73
views
Is there an axiomatic system for propositional logic that does not use modus ponens as a rule?
Is there an axiomatic system for (classical) propositional logic that does not use modus ponens as a (primitive) rule?
I would be particularly interested in a derivation of it from some other set of ...
- 105
0
votes
1
answer
56
views
Types of Logic/ proofs
I am having a hard time understanding the difference between classical, constructive, predicate, intuitionistic and propositional logic.
I know that propositional logic studies ways of joining ...
4
votes
0
answers
58
views
Are soundness and completeness a part of proof theory, model theory or something else?
I have a question that I hope can clarify the scopes of model theory and proof theory. I have the following naïve understanding of the two areas (please correct me if I'm wrong):
Model theory is ...
- 61
1
vote
0
answers
44
views
Prove that propositional Aczel slash is closed under deduction
I have already proved that
$ \Gamma |\phi \Rightarrow \Gamma \vdash_{IPC} \phi $.
On the other hand, I have tried to prove the other side. I used induction on the length of the proof.(I used natural ...
2
votes
1
answer
84
views
How exactly are you allowed to use free set/predicate variables in first-order arithmetic?
In first-order arithmetic, you can't quantify over sets of numbers. However, you can include sets as free variables. I don't think this is just a meta-linguistic thing, as I've read papers about Peano ...
- 21
2
votes
4
answers
273
views
Why is Q → P a logical consequence of ¬(P → Q )
I don't want to ask my professor about this because I'm awful at this and he's not the, uhh, patient type of professor to say the least.
Anyhow, it was my understanding that ...
- 23
36
votes
3
answers
3k
views
Under the Curry-Howard correspondence or loosely "proofs-as-programs", do we also have "programs-as-proofs" and what would some arb. program prove?
Curry-Howard Correspondence
Now, pick any 5-30 line algorithm in some programming language of choice.
What is the program proving? Or, do we not also have "programs-as-proofs"?
Take the ...
- 19.5k
5
votes
2
answers
172
views
Prove that a construction exists: is this a constructive proof or existential proof?
This top answer claims that it is possible to prove that a constructive proof cannot exist.
I think, if "non-existence of constructive proof" can be proven, then for some other questions, it ...
- 2,944
1
vote
1
answer
174
views
Natural Deduction Proof search algorithm for Classical Propositional logic?
I know of two algorithms for determining classical propositional validity:
Convert the problem into a SAT problem, run a SAT solver. These algorithms are efficient, but it seems difficult/infeasible ...
- 99
2
votes
1
answer
73
views
What is the relevance of the fast-growing hierarchy in the definition of Yudkowsky’s number?
I’m struggling with a certain connection the author draws in defining a certain “huge” number. The number is defined as follows:
Let T be the first-order theory of Zermelo-Fraenkel set theory plus the ...
- 305
0
votes
1
answer
41
views
Finding an Example for the following claim in Propositional Calculus?
Let $\Sigma$ be in $WFF$, we say $\Sigma$ is closed if for every $a$ in $WFF$ if $\Sigma \vDash a$ then $a$ in $\Sigma$.
Claim:
For every $\Sigma_1, \Sigma_2$ in $WFF$ such that $\Sigma_1$ is closed
...
- 21
1
vote
0
answers
55
views
How to prove the tautology $\neg\exists x\varphi\leftrightarrow \forall x\neg \varphi$ according to Halbeisen and Krapf's book
I'm studying some basic features of Proof Theory in the recent "Gödel's Theorems and Zermelo's Axioms", by Halbeisen and Krapf. In this book, the authors introduce a list of logical axioms ...
- 1,819
3
votes
1
answer
63
views
Clarification regarding substitution in sequent calculus
Wikipedia's Sequent Calculus article states:
$A[t/x]$ denotes the formula that is obtained by substituting the term $t$ for every free occurrence of the variable $x$ in formula $A$ with the ...
- 1,059
3
votes
1
answer
81
views
What are the syntactic restrictions on proof by contradiction?
I am reading Natural Logic by Neil Tennant and I am met with this example of proof by contradiction.
It bothers me that the premise ~Ga was introduced seemingly ...
- 611
4
votes
0
answers
55
views
Gaps between intutionistic and classical arithmetic
Let $\mathrm{I}\Sigma_n$ stand for the classical theory of Robinson arithmetic + bounded induction + induction on $\Sigma_n$ formulas. Let $\mathrm{CI}\Sigma_n$ stand for the intuitionistic theory of ...
- 349
1
vote
1
answer
40
views
If a metatheory proves consistency of a theory, will consistency of the metatheory suffice?
I'm going to call a metatheory reasonable if it's consistent and whenever there exists a proof for a sentence $\phi$ from a theory $T$ the metatheory proves $T\vdash \phi.$
Suppose that some ...
- 3,695
2
votes
0
answers
44
views
What is quantifier-free induction over initial segments?
I am currently reading the section on Gentzen's Consistency Proof in this article on Proof Theory from the Stanford Encyclopedia. There it says:
Given a natural ordinal representation system $\langle ...
- 903
4
votes
1
answer
135
views
Why do we need ordinal representation systems?
Trying to learn about ordinal analysis and I keep seeing the concept of the natural ordinal representation system, for representing ordinals as relations on N. In particular the definition of an ...
- 305
0
votes
0
answers
35
views
Is the intuitionistic absurdity rule $\bot E$ necessary to prove that a theory $\mathcal{T}$ is consistent?
In Elements of Intuitionism (p. 145), Dummett wrote:
Cut-elimination is directly connected with establishing consistency, and was so intended by Gentzen. Given the equivalence of N and L, acceptance ...
1
vote
1
answer
73
views
Different textbooks, different formulations of the Deduction Theorem: sometimes the formula in the antecedent need to be closed, sometimes not. Why? [duplicate]
For clarity, let me take two examples: Shoenfield's Mathematical Logic, and Enderton's A Mathematical Introduction To Logic. Well, in those texts we have two different Deduction Theorems (we are in ...
- 93
3
votes
0
answers
119
views
Open problems in Proof theory and Logic
There are numerous questions in the same form: "What are some open problems in mathematical logic". So for this we know:
Shelahs "Logical Dreams"
Logical Dreams
Friedmans "102 ...
1
vote
1
answer
93
views
How to derive $\prod x: \text{Nat}, Id(S(x), O) \to \bot$ in Intensional Type Theory
In HoTT Lecture, https://www.youtube.com/watch?v=VWmXF-P4-Z8&list=PL1-2D_rCQBarjdqnM21sOsx09CtFSVO6Z&index=7, Harper introduced a dependent form of recursion rule:
$$
\Gamma \vdash M : Nat ~~~ ...
2
votes
1
answer
72
views
When first encountering a set of primitive inference rules, how do we approach the derivation of the very first derivable inference rules?
I'm currently learning Ebbinghaus et. al.'s propositional calculus in their book Mathematical Logic, and I'm trying to derive the very basic rules of inference such as $\land$ introduction, the law of ...
- 698
0
votes
1
answer
149
views
An effective procedure to disproof Church-Turing thesis?
Suppose that an effectively axiomatized consistent formal system P that contains enough arithmetic for Gödel's Incompleteness theorems to apply,
proves for any undecidable formula φ in the language of ...
- 3
1
vote
1
answer
96
views
Applying law of excluded middle to a theory-independent sentence
In $ZF$ (or $ZFC$) let's take a sentence $S:= CH\vee \neg CH$, where $CH$ is the continuum hypothesis. Then $S$ has trivial proof, namely application of the law of the excluded middle ($LEM$). On the ...
- 359
2
votes
1
answer
55
views
Undo a weakened statement in sequent calculus later in the inferences
I'm working on an answer to (b) of Mathematical Logic, Ebbinghaus et. al. 1984 p. 64
Consider the following inference:
$$
\frac{\begin{align}\Gamma \vdash A\\ \Gamma \vdash B\end{align}}{\Gamma \vdash ...
- 698
2
votes
1
answer
80
views
Are there any proof-size-aware logics?
I'm aware of provability logics which have a notation $\square P$ for "$P$ is provable", but I'm not aware of one which is more 'fine grained' and has a notion of proof term size (e.g. with ...
- 23
0
votes
1
answer
134
views
Proof of nonexistence of purely algebraic proof of the Fundamental Theorem of Algebra.
There have been questions before on Math SE about whether there is a purely algebraic proof of the FTA. But as far as I know, nobody has proven rigorously that there is no purely algebraic proof. Has ...
- 13.3k
1
vote
0
answers
114
views
Do all provable theorems have a finite number of proofs?
The Pythagorean Proposition states that there are 367 proofs of Pythagoras' theorem. Is there a limit for the number of proofs of this, or any, theorem? Are there provable theorems with infinitely ...
- 13
3
votes
0
answers
53
views
Comparing two semantics, equivalent in the global sense, not in the local sense?
I am working on a project that involves a deductive system $\vdash$, with two model-theoretic semantics $\models_A$ and $\models_B$, for which $\vdash$ is sound and complete. That is,
$\Gamma \vdash \...
- 317
0
votes
0
answers
36
views
Essential use of case analysis with theorem which is independent of ZFC
The continuum hypothesis ($CH$) is known to be independent of ZFC.
Is it possible that some mathematical theorem $P$ has a proof of the form:
...
- 7,856
0
votes
0
answers
82
views
What type of algebraic structure is logic?
What does Mathematica study?
Answer: Structures; Sets where there are defined relations and functions.
It happens that some of these structures contain others, and I think that logic is the structure ...
0
votes
0
answers
32
views
A question on a specific kind of prenex normal form
We say that a first-order formula is in DNF if it can be obtained from a propositional formula in DNF by replacement of propositional variables with atomic predicate formulas. We say that $A$ is in ...
- 1,031
1
vote
1
answer
49
views
Sequent type system in which all formulae are closed
In most presentations of the sequent calculus, the formulae that appear in a sequent $\Delta \vdash \Gamma$ may be open; i.e., may have free variables.
I am looking for elegant presentations of ...
- 473