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.
842
questions
0
votes
0answers
47 views
Recommendation for graduate school in mathematical logic [closed]
I am a graduate student studying algebraic geometry for a MS degree.
For my PhD I want to study mathematical logic and in particular, automated theorem proving.
Would there be a good recommendation of ...
0
votes
0answers
37 views
Single sxiomatizability of r.e. extensions.
Beklemishev proves following lemma in [1]
Lemma 2.21. Let $U$ be a consistent r.e. extension of $T$ of comlexity $\Sigma_n$. Then there is single $\Sigma_n$-sentence $\varphi$ such that $T+\varphi$ ...
6
votes
1answer
140 views
World's smallest (Exception-based) proof-checking language (in Python). In what way is Coq, Lean, Isabelle “better”? [closed]
As you may already know, the codebases written for Coq, Lean, etc. are humungous. Thus a goal in a new proof assistant might be to simplify things. Suppose we restrict our attention not to general ...
0
votes
1answer
38 views
First order logic reference request
I need a textbook (or any other material) about first order logic, that includes these precise parts: $LK$ sequent calculus, and substitution. I already searched on Shoenfield and Mendelson and I didn'...
1
vote
0answers
41 views
A formal definition of circular proofs.
Suppose one were to prove that $\pi$ is irrational by claiming "because it is transcendental". This proof would be seen as circular. However, neither of "$\pi$ is irrational" and &...
5
votes
1answer
706 views
Hierarchy in logical systems
I had an informal conversation in which I was told that logical systems could be intuitively drawn in a hierarchy according to their expressive power, i.e. the amount of things we can prove with them. ...
2
votes
0answers
44 views
Functions which are provably total in second order peano arithmetic
Girard has a representation theorem claiming:
The functions representable in $F$ are exactly those which are provably total in second-order peano arithmetic $PA_2$.
I believe the usual way to prove ...
4
votes
1answer
68 views
A question about the (un)derivability of Cut Rule in Sequent Calculus
This question is motivated by a previous discussion regarding How to show that a valid rule is not derivable in Intuitionistic propositional calculus.
The reference is to Gentzen (1934-35)'s Sequent ...
1
vote
0answers
64 views
Can a proven theory be false if its premise is false?
Background
When I was learning Math on Khanacademy, the teacher gave a brief demonstaration about the difference between 'theorem' and 'postulate/axiom'. He indicated that 'postulate' and 'axiom' ...
7
votes
2answers
85 views
If I can prove $Y$ from “$X$ is true” and from “$X$ is false”, can I prove $Y$ without using $X$ at all?
Suppose I have a statement $X$, for which I do not know whether it is true or false. And suppose further that I want to prove a statement $Y$:
I first assume that $X$ is true, and I construct an ...
9
votes
3answers
930 views
What is the point of model theory?
Wikipedia defines model theory as ...
... the study of the relationship between formal theories (a collection of sentences in a formal language expressing statements about a mathematical structure), ...
1
vote
0answers
42 views
Which context weakening rules are derivable in this system of equational logic?
I am trying to work through Andrew Pitts' chapter on categorical logic: Categorical Logic. On page 7 he presents a system of equational logic. The rules are listed below:
$$\dfrac{}{M = M : \sigma \ [\...
2
votes
1answer
58 views
Generalized Deduction Theorem
In my comment on this question, I mentioned that there was a generalized form of the deduction theorem that looks something like this
For any finite set of formulae, $\Gamma$
$$\dfrac{\Gamma\vdash\...
2
votes
1answer
54 views
Incompleteness Theorems for Limit-Computable Formal Systems
Godelās First and Second Inconpleteness Theorems are about Peano Arithmetic, but their punchlines are respectively that āAny sufficiently expressive computable formal system cannot be complete and ...
3
votes
1answer
81 views
What does it mean to some logical statement to be provable and decidable?
I am not a mathematician and trying to get deeper insight into modern logic.
It happens all the time, that statements like statement P is unprovable arise, or, more ...
2
votes
2answers
167 views
What are the pros and cons of natural deduction relative to Hilbert-style systems?
What are the pros and cons of natural deduction relative to Hilbert-style systems?
From Wikipedia, I get the impression that natural deduction proofs tend to be shorter and closer to how humans do it. ...
2
votes
2answers
117 views
Is there any finite deductive system for propositional logic which only uses unary rules?
I'm not sure if this has ever been proven/disproven, but, assuming the usual grammar of propositional logic, is there any deductive system which derives exactly the tautologies of classical logic ...
4
votes
4answers
205 views
Is there an object such that its unique existence follows from choice axiom, while its existence cannot be proven without choice axiom?
Let $\varphi$ be a formula, and suppose $\text{ZFC}\vdash \exists x\varphi(x)\wedge\forall x\forall y(\varphi(x)\wedge\varphi(y)\to x=y)$
Is $\text{ZF}\vdash \exists x\varphi(x)$ true?
0
votes
2answers
53 views
How to establish the modus ponens inference rule in the LK sequent calculus for first-order logic? [closed]
How can the modus ponens inference rule
$$
\frac{\Gamma \vdash \varphi\hspace{1cm}\Delta\vdash \varphi\rightarrow\psi}{\Gamma,\Delta \vdash \psi}
$$
be established in the LK sequent calculus for first-...
1
vote
0answers
34 views
Is there such thing as “bounded” Induction?
Consider, for example, a simple result in group theory. Let $\sigma=(a_1 \ a_2 \cdots a_k )$ be a cyclic permutation in $S_n$. I wish to show that $\sigma^{i}(a_1)=a_{i+1}$ for all $i\in\{0,1,\dots,k-...
4
votes
0answers
76 views
Can ZFC decide more values of the Busy Beaver function than PA?
This is related to a previous question. In that question, I asked whether ZFC can define the Busy Beaver function. I was told even Peano Arithmetic(PA) can define it, and also that PA can't decide ...
7
votes
2answers
520 views
What theory of logic or types considers the “category of propositions”?
Was wondering if there was a theory already out there that considers the "category $\text{Prop}$ of propositions". It is a preorder (at most one arrow between two propositions), in which $A ...
7
votes
1answer
239 views
I'm probably wrong about Curry-Howard
Here's my problem : I know from Curry-Howard that simply typed lambda-calculus is isomorphic to natural deduction.
Now I know that natural deduction admits cut-elimination. I also know that the ...
0
votes
1answer
72 views
What is a formula $\phi$ which satisfies $\vdash \phi$ called?
In a logic system, a formula which holds under all interpretations is called a tautology (e.g. in propositional logic) or valid formula (e.g. in FOL).
Is there a name for a formula $\phi$ which ...
2
votes
1answer
94 views
Do inference rules mean the same in a Hilbert system and in a natural deductive system?
Is it correct that Enderton's A Mathematical Introduction to Logic uses a Hilbert style system for first order logic?
On p110 in SECTION 2.4 A Deductive Calculus in Chapter 2: First-Order Logic
Our ...
2
votes
1answer
127 views
Does sequent calculus have axiom?
Are axioms inference rules without assumptions, or not inference rules at all?
I heard that sequent calculus doesn't have axioms, is that true?
p69 in Ā§6. Summary and Example in IV. A Sequent ...
2
votes
1answer
105 views
What does “prove” mean?
What does "prove" mean?
I am using the following examples to understand the general cases. I don't know how to articulate my questions in the general case.
I was wondering about at what ...
4
votes
0answers
45 views
Has something like the Turing Machine that halts if ZFC is inconsistent been done for other axiom systems?
The current best result (as far as I could find) is that there exists a $748$-state Turing Machine that halts iff ZFC contains a contradiction. Are there any similar results for other axiom systems, e....
5
votes
0answers
105 views
Can all $\mathsf{Q}$-provably recursive functions be “frequently termlike”?
Now asked at MO.
Motivated by this question, I'd like to ask whether in a precise sense there are no "interesting" functions which are provably recursive in Robinson's arithmetic $\mathsf{Q}...
2
votes
1answer
108 views
Provably total functions in $\mathsf{Q}$
I was interested in the relations between induction and recursion, and so a natural question (to my mind, anyway), was how much we can prove without appealing to induction, i.e. which functions are ...
0
votes
1answer
71 views
grid “proof” for commutativity of multiplication
In this write-up by Tim Gowers on why multiplication is commutative,
https://www.dpmms.cam.ac.uk/~wtg10/commutative.html
he gives a physical grid model to which multiplication corresponds and says - &...
6
votes
1answer
177 views
Kaye-Wong paper Theorem 6.5
In the paper On Interpretations of Arithmetic and Set Theory of Kaye and Wong they say that Theorem 6.5 (that PA can be interpreted in ZF-Inf*, that is, ZF plus every set is contained in a transitive ...
3
votes
1answer
55 views
Proving $\forall x \neg P(x) \implies \neg \exists y P(y)$ in sequent calculus
Having the inference rules
$$ \frac{\Gamma, A[x:t] \implies \Delta}{\Gamma, \forall x A \implies \Delta} \forall L $$
$$ \frac{\Gamma, A[x:y] \implies \Delta}{\Gamma, \exists x A \implies \Delta} \...
6
votes
1answer
152 views
Epsilon recursion and ZF-Inf+TC in the Inverse Ackermann Interpretation
In the paper On Interpretations of Arithmetic and Set Theory of Kaye and Wong they write:
Equipped with $\in$-induction, we obtain an inverse interpretation of
PA in ZFāInf*. The plan is to define a ...
5
votes
1answer
76 views
Does an inference rule under natural deduction operate on sequents or formulas?
In natural deduction, is it correct that an inference rule operates on sequents which have only one formula on their right hand sides?
Why does an inference rule seem to operate on formulas in Hurley'...
4
votes
1answer
148 views
Interpreting $\textbf{PA} + \neg\text{Con}(\textbf{PA})$ in $\textbf{PA}$
How does one interpret $\textbf{PA} + \neg\text{Con}(\textbf{PA})$ in $\textbf{PA}$, and what is the significance of such an aberrant interpretation?
I'm interested in the following: $\textbf{ZF} - \...
4
votes
2answers
136 views
How can you derive a formula without premises? [duplicate]
What is the difference between $\vdash A $ and $\models A$?
I'm not asking about the general difference between syntactic entailment and semantic entailment.
I specifically don't understand the ...
2
votes
0answers
61 views
Concrete examples of statements not provable in PRA + $\epsilon_0$-induction that are provable in PA?
It is well-known that $\mathbf{PRA}$ plus $\epsilon_0$-induction on bounded formulas cannot prove all $\mathbf{PA}$ theorems (essentially because $I\Sigma_1$ plus $\epsilon_0$-induction on bounded ...
3
votes
1answer
84 views
What is the definition of “a derivation of a sequent ”?
In Chapter IV. A Sequent Calculus in Ebbinghaus' Mathematical Logic, a sequent is defined as:
If we call a nonempty list (sequence) of formulas a sequent, then we can use sequents to describe "...
2
votes
1answer
99 views
How to derive ${ A \vdash C }$ from ${A \lor B \vdash C}$ in the sequent calculus LK?
How to derive ${ A \vdash C }$ from ${A \lor B \vdash C}$ in the sequent calculus LK? It seems obvious that if ${A \lor B \vdash C}$ is true, then ${ A \vdash C }$ is true.
There are rules
$\cfrac {...
6
votes
1answer
100 views
Is Goodstein's theorem equivalent to $\varepsilon_0$-induction over weak base theories (e.g. PRA)?
Is Goodstein's theorem equivalent to $\varepsilon_0$-induction over a weak base theory like PRA? I'm surprised this hasn't been asked here before (as far as I can tell).
4
votes
4answers
221 views
Is law of excluded middle necessary in this proof?
I'm currently learning natural deduction and here is my question.
Is it possible to prove this
$\vdash \neg(P \land Q)\rightarrow (\neg P \lor \neg Q)$
without referring to the law of excluded middle ...
4
votes
1answer
86 views
Interpretation of one theory in another
I'm reading a review of Nelson's book "Predicative Arithmetic". In the review Wilkie writes:
Of course the spirit of the program is that a sentence, $A$, is to be
regarded as predicatively ...
0
votes
1answer
74 views
Is non-capture avoiding substitution permitted in the lambda calculus?
In the lambda calculus (typed and untyped) "capture-avoiding substitution" is often defined. But this doesn't rule out non-capture avoiding substitutions unless we require that all ...
1
vote
1answer
84 views
deduction proof
Prove $p \wedge \neg p \vdash q$ for any propositional variables $p$ and $q$ without using disjunctive syllogism or excluded middle or $\neg$-elimination.
I can prove this easily using $\neg$-...
4
votes
1answer
103 views
First order logic natural deduction problem
I am struggling with a particular case in the (inductive) proof of Theorem 2.8.3 (i) of Logic and Structure by Dirk Van Dalen ($c \neq x$ in the Theorem statement is a variable)
The cases when we ...
4
votes
0answers
69 views
Every provably recursive function in PA is bounded by a Hardy function
The following lemma and proof are from Takeuti's Proof Theory (2nd edition, pp. 126-127), I've highlighted the problematic part in blue:
How does Takeuti get this inequality? If the proof $x$ is not ...
4
votes
0answers
82 views
Characterization of provably recursive functions in PA
This concerns Takeuti's Proof Theory: the book contains a lot of wonderful material, but the presentation is sometimes lacking (and so many typos!). At least that has been my experience so far, ...
1
vote
1answer
112 views
While using the method of proof by contradiction, are we “assuming” consistency?
I am aware of threads here and here which asks something similar. However, I had something very specific to ask under the same context.
I have a very elementary question about the connection between ...
1
vote
2answers
101 views
Help to find a proof in natural deduction
I have a question about the methodology of natural deduction, more specifically finding a proof in natural deduction.
The assignment says:
Find a proof for the formula $(P \rightarrow \neg P) \...
