Skip to main content

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
14 votes
3 answers
2k views

A seemingly contradictory function - where's the issue?

I have constructed a function of seemingly contradictory nature. Let $f$ be a function which, given an input $n\in \mathbb{N}$, lexicographically searches through all strings and finds the $n$th pair $...
volcanrb's user avatar
  • 2,954
0 votes
1 answer
118 views

If $\textbf{x}$ is not free in $\textbf{A}$, show that $\vdash\exists\textbf{x}\textbf{A}\leftrightarrow\textbf{A}$

Let $A$ be a formula in a theory $T$. Then $\vdash_{T}\exists xA$ certainly shouldn't imply $\vdash_{T}A$ if $x$ is free in $A$, but I don't see what's wrong with the following proof. $\textbf{Lemma}$....
SihOASHoihd's user avatar
  • 1,894
4 votes
1 answer
147 views

Notion of proof for first-order formulas with parameters

When proof in first-order logic is formalized by the statement $T\vdash\phi$, it is required that $T$ is a set of sentences, i.e. formulas with no parameters. Gödel's completeness theorem states that ...
C7X's user avatar
  • 1,271
1 vote
2 answers
123 views

Can sequents in the sequent calculus contain free variables?

In chapter 14 of Computability and Logic (fifth edition) a proof procedure, specifically a sequent calculus, is introduced. The text states on page 168 that "A sequent $\Gamma\Rightarrow\Delta$ ...
Joe's user avatar
  • 19.9k
4 votes
0 answers
96 views

Show that Proof by Contradiction rule is derivable from all instances of it with atomic conclusion

The problem shows up in Troelstra's Basic Proof Theory, exercise 2.3.6A. Show that in [classical logic's Natural Deduction], for the languages without ∨, ∃, all instances of ⊥c derivable from ...
confusedcius's user avatar
3 votes
0 answers
116 views

Automated theorem proving and set theory

I already know a few things about theorem proving however I was wondering how to use this when we are dealing with a non finite amount of axioms. In particular I was hoping to understand how to use ...
Le Grand Spectacle's user avatar
1 vote
0 answers
37 views

What is the correct way to encode the 2nd projection of a dependent pair type?

Consider the following Church-encoded definition for a dependent pair type (a.k.a. existential type) in a pure type system such as the Calculus of Constructions: $$\operatorname{Exists} \;\; := \;\; \...
cp289's user avatar
  • 11
1 vote
1 answer
96 views

Set-theoretic semantics for sigma types

I'm trying to understand the set-theoretical semantics of sigma types. Suppose $\Gamma\vdash A : \text{type}$, $\Gamma.A\vdash B:\text{type}$, $\Gamma\vdash a:A$, $\Gamma\vdash b:B[1.a]$, $\Gamma\...
user837242's user avatar
1 vote
1 answer
58 views

Examples of sequent derivations that uses cut rule that can be modified to not to use cut rule?

The cut-elimination theorem states that any sequent calculus derivation that uses the cut rule also has a derivation that does not use the cut rule. I cannot find any explicit examples of such ...
John Davies's user avatar
1 vote
0 answers
26 views

Double exponentials in weak arithmetic

In arithmetic without total exponentiation, the exponentiable numbers are closed under addition. It is thus common to think of natural numbers as binary strings $n : |n| \to 2$, whose (unary) lengths $...
Robin Saunders's user avatar
1 vote
1 answer
68 views

Why doesn't $RCA_0$ prove $\Sigma^0_1$-comprehension?

Answer: because that's $ACA_0$, alright, but: Friedman et al.'s 1983 "Countable algebra and set existence axioms" has [verbatim, including old terminology and dubious notation]: Lemma 1.6 ($...
ac15's user avatar
  • 1,064
0 votes
2 answers
161 views

Consistency of Theory and Deduction Theorem

Let $\Gamma$ be a consistent theory of propositional logic and $\varphi$ a propositional formula. It is well known that $\Gamma \cup \{\neg\varphi\}$ is consistent if $\Gamma \not\vdash \varphi$. A ...
yue's user avatar
  • 65
2 votes
1 answer
74 views

Use sequent calculus to show if $\Gamma\vdash t_1=t_2$ then $\Gamma\vdash f(t_1)=f(t_2)$

Suppose the sequent $\Gamma\vdash t_1=t_2$ where $t_1,t_2$ are closed terms. Let $f$ be a one-place function symbol. I am trying to find a sequent calculus derivation of $\Gamma\vdash f(t_1)=f(t_2)$ ...
John Davies's user avatar
1 vote
1 answer
80 views

Double negation in sequent calculus

Kind of related to this post. I wonder if it is possible to derive $\Phi\vdash\Delta$ from $\lnot\lnot\Phi\vdash\Delta$ using standard sequent calculus elimination rules. I am not sure where to start. ...
John Davies's user avatar
3 votes
1 answer
96 views

Question about quantifiers in the proof of the cut eliminiation theorem

Lately I have been reading about the cut elimination theorem, I think I get the idea however I have been struggling with some technical details concerning quantifiers. Consider the following rule: ...
Le Grand Spectacle's user avatar
0 votes
0 answers
30 views

What's the natural metric/topology on infinite derivations?

In the appendix to the SEP Proof Theory article, Michael Rathjen makes reference to a topology on infinite derivations for which a variant of cut-elimination is a continuous function. The referenced ...
Alvaro Pintado's user avatar
0 votes
0 answers
43 views

Is this a valid way to prove a premise false?

Let P signify that X is algebraic and not equal to 0. Let Q signify that e raised to the X is algebraic. $$1.\exists X(P(X)\land Q(X))$$ $$C.\forall X\exists X_1\left(P\left(X\right)\rightarrow Q\left(...
user avatar
5 votes
0 answers
172 views

Proving $\exists x[P(x)] \to \exists y[\exists x[P(x)]\to P(y)]$ in for intuitionistic $\varepsilon$-calculus.

I am researching Mint's paper: Intuitionistic Existential Instantiation and Epsilon Symbol (this is as far as I know unfinished work) In intuitionistic logic, it is not difficult to prove that $$\...
Tungsten's user avatar
  • 130
3 votes
1 answer
86 views

Are there examples of statements not provable in PA that do not require fast growing (not prf) functions?

Goodstein's theorem is an example of a statement that is not provable in PA. The Goodstein function, $\mathcal {G}:\mathbb {N} \to \mathbb {N}$, defined such that $\mathcal {G}(n)$ is the length of ...
Burnsba's user avatar
  • 1,025
3 votes
1 answer
135 views

What is the metatheory required for proving the cut-elimination theorem for classical logic? Is the proof circular?

I am new to proof theory, and I am curious about the tools required in the proof of cut-elimination for the sequent calculus. I understand how the proof operates informally: a main induction on the ...
MotDave's user avatar
  • 33
3 votes
1 answer
97 views

Computational Complexity of Equational Logic

Equational logic uses a surprisingly small set of axioms to prove all algebraic identities (algebraic in the sense of universal algebra, so things like field theory fall beyond this scope). This makes ...
Thomas Anton's user avatar
  • 2,336
1 vote
0 answers
94 views

The provability predicate in incompleteness theorem [duplicate]

The prooffor(x,y) predicate in godel's 1st incompleteness theorem is primitive recursive, so if there is a statement ' S ' within the theory , which would be 1st order PA in godel's case , and it has ...
user avatar
3 votes
1 answer
60 views

Michell FPL 2.3.5 (observable types)

(a) Show that the relation of observational equivalence remains the same when changing the observable types of pcf from nat, bool to nat. (b) Further show that changing from nat,bool to nat, bool, ...
emesupap's user avatar
  • 668
1 vote
1 answer
43 views

What is the correct way to interpret the Intuitionistic rules of Kleene's sequent (Gentzen) system G1 (in sec. 77 of Kleene I.M. 1952)

I'm having difficulty understanding the sequent/Gentzen proof system in section 8 of a paper by Gurevich [G1977], and he defines that system by telling the reader to modify the system G1 from Kleene's ...
tuiowalu's user avatar
4 votes
1 answer
443 views

Are there axioms in a natural deduction system?

In the Hilbert system, a proof may include some axioms. In a natural deduction system, it seems no axiom is involved, at least from the examples I read in logic books. So, I wonder how axioms such as ...
William's user avatar
  • 233
6 votes
1 answer
251 views

How to prove that Peirce's law does not hold in this logical system?

I consider a Hilbert system defined by the following: $A \rightarrow (B \rightarrow A)$ $(A \rightarrow (B \rightarrow C)) \rightarrow ((A \rightarrow B) \rightarrow (A \rightarrow C))$ I believe this ...
Le Grand Spectacle's user avatar
1 vote
0 answers
82 views

Are finitist systems the ones with a proof-theoretic ordinal of at most $\omega^\omega$?

The proof-theoretic ordinal of $\mathsf{EFA}$ and $\mathsf{RCA}_0^*$ are $\omega^3$ and the one of $\mathsf{PRA}$, $\mathsf{I\Sigma1}$, $\mathsf{RCA}_0$, etc. is $\omega^\omega$. See https://ncatlab....
user avatar
0 votes
0 answers
96 views

Motivations for introducing a "super-universe"

I'm trying to understand universes in type theory, and I'm looking at this note. Let's consider a toy example, where we have just two universes, $U_0$ and $U_1$. Then we have this set of rules (...
user837242's user avatar
1 vote
3 answers
81 views

Given an axiomatics, can you use its model to prove a theorem in that axiomatic?

My point is, it is possible that a sentence is true in one model and false in another (e. g. the 5th euclidean axiom). So there exist theorems that are only true in some of an axiomatics' models. So ...
Sherlock Holmes's user avatar
2 votes
0 answers
41 views

Alternative formation/ notation for axiom of mathematical induction

I hope to clarify the difference between the following two statements: $S\subset \mathbb{N}$ (set of natural numbers), $\forall n \in \mathbb{N}, \text{ if } n\in S \text{, then } n+1\in S$ $\forall ...
Sean's user avatar
  • 53
1 vote
0 answers
60 views

Is a proof one kind of computation?

Is proving mathematical theorems one kind of computing? I read somewhere in a book that proofs are one kind of computation. I am not talking about formal proofs, I am talking about the informal ...
user107952's user avatar
  • 20.9k
3 votes
3 answers
218 views

What is an example of a proof that uses the principle of explosion/ex falso quodlibet?

I am reading through Mathematical Logic by Ian Chiswell and Wilfrid Hodges. In chapter 2 they introduce natural deduction rules. Before stating a rule, the authors (usually) motivate the rule by ...
Artyom Elessar's user avatar
2 votes
0 answers
87 views

What means to say that a result depends on a theorem?

In everyday talk we say things like: we must use the fundamental theorem of calculus to calculate this integral; we must use the results of analysis to proof the fundamental theorem of algebra; we ...
Lost definition's user avatar
2 votes
1 answer
112 views

How exactly does completeness imply compactness?

The general argument goes like so: suppose $\Sigma$ is finitely satisfiable, but not satisfiable. Therefore, $\Sigma$ is inconsistent, so $\Sigma \vdash \bot$. Then, by completeness, there exists a ...
zaq's user avatar
  • 874
1 vote
0 answers
27 views

Extending Takeuti's proof of the completeness theorem to sentences with constants.

In Takeuti's Proof Theory, the completeness theorem is proven only for sequents which contain no constants (or any other terms other than variables) in any of their formulas. Here is the author's ...
zaq's user avatar
  • 874
1 vote
0 answers
89 views

Is there a sensible first order expression meaning that every set in $\omega$ is some set-theoretical natural number?

Motivation: With the following I want to understand the relationship between the set-theoretical natural numbers 0,1,2,... and the set of natural numbers $\omega$ better. Let 0 := $\emptyset$, 1 := {$\...
Hypatius's user avatar
1 vote
2 answers
303 views

Is it legitimate to assert a propositional function?

About one and a half years ago, I had a dispute with someone over whether it is legitimate to assert a propositional function, as in $ \vdash x = x $. They said an assertion containing free variables ...
Bulhwi Cha's user avatar
11 votes
2 answers
1k views

Proving there is only one proof?

I cannot seem to find or come up with an answer to the following question: In mathematics, is it possible to prove that there is only one (shortest) proof of a given theorem (say, in ZFC)? Are there ...
Alex's user avatar
  • 353
0 votes
0 answers
38 views

Does Substitution of Logical Equivalents hold for minimal logic?

Suppose that minimal logic proves that $\psi_1\leftrightarrow\psi_2$, does it follow that minimal logic proves $\varphi[\theta/\psi_1]\leftrightarrow\varphi[\theta/\psi_2]$?
IllogicalUser's user avatar
3 votes
1 answer
76 views

Abstract conditions for a formal system to be adequate with respect to the standard semantics

In general, when introducing logic, we present students with a given formal system (e.g. Hilbert-style axioms, natural deduction, sequence calculi, etc.) and then, after presenting the standard ...
Nagase's user avatar
  • 5,497
1 vote
0 answers
33 views

Double Induction on Premises of a Rule of Inference

I am working through the proof of a theorem about a derivation system. The theorem requires an induction derivation trees that end with a rule $R$ which has two premises $P_1$ and $P_2$. The proof ...
IllogicalUser's user avatar
6 votes
0 answers
103 views

Who is the "$\Pi_2$-soundness" version of the first incompleteness theorem due to?

I'm trying to remember who is responsible for the following well-known weak version of the first incompleteness theorem: Suppose $T$ is a c.e. consistent $\Pi_2$ extension of Robinson's $\mathsf{Q}$ (...
Noah Schweber's user avatar
0 votes
1 answer
169 views

What are the merits of having a "good" proof system?

Background: My understanding is that model-theoretic semantics (MTS) and proof-theoretic semantics (PTS) differ in the following ways. In MTS, you first define the notion of truth in models and then ...
user avatar
4 votes
0 answers
194 views

Examples of statements which, if true, have unreasonably long proofs

In $\mathbf{Q}$ (or any theory strong enough to encode $\mathbf{Q}$), there exist true statements whose proofs cannot be written in under $N$ symbols for a fixed $N$. For example, if $N = 1000000$ ...
mattematician 's user avatar
2 votes
0 answers
33 views

Equivalence of Martin-Löf sequent calculus and standard sequent calculus with material implications

I have a question about the proof system of Per Martin-Löf, developed in his paper "Hauptsatz for the intuitionionistic theory of iterated inductive definitions". In this paper, Martin-Löf ...
RobbeVB's user avatar
  • 21
1 vote
1 answer
69 views

Establishing $\Gamma, A: Type \vdash (A)Type\ \textbf{kind}$ in LF

This is a follow-up to my previous question. Consider the same LF as in that question: LF is a simple type system with terms of the following forms: $$\textbf {Type}, El(A), (x:K)K', [x:K]k', f(k),$$ ...
user avatar
3 votes
1 answer
208 views

Why use LF to define type theories?

I'm trying to understand the notion of a logical framework and how/why/when it's used to define type theories. I'm looking at Luo's "Computation and Reasoning" (1994), where he considers LF, ...
user avatar
1 vote
0 answers
59 views

Reflection principle for finite subsystems of PA.

I would like to clarify the reasoning behind the proof of reflection schema for finite subsystems of PA that I found in "The Blind Spot" book. To be wore precise, we have a finite subsystem $...
A. G's user avatar
  • 328
1 vote
0 answers
36 views

Standard coding in elementary arithmetic

Does anyone know a reference discussing/describing the coding of sets and finite sequences in Elementary Arithmetic (EA, also know as $I\Delta_0(exp)$)? All I know is that $\#\emptyset=0, \#\{n_1,…,...
Ingolfur's user avatar
  • 153
5 votes
0 answers
88 views

When should one use transfinite induction?

I've come across it multiple times now in proof theory papers that authors use (sometimes quite elaborate) inductions in order to prove easy results. The most striking example is the following, where ...
10012511's user avatar
  • 682

1
2 3 4 5
20