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.

Filter by
Sorted by
Tagged with
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) \...

1
2 3 4 5
17