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-* ...

learn more… | top users | synonyms

9
votes
4answers
349 views

How or why does intutionistic logic proof negations from within the theory, constructively?

I'm having a little of a cognitive dissonance why, in intuitionistic logic, it's possible to show stentences like $(\neg A \land \neg B) \implies \neg(A\lor B).$ In plain text: If 'A isn't true' as ...
0
votes
2answers
60 views

Why this first-order logic formula is not correct?

I'm studing computer science at university, in specific Artificial Intelligence. We are using Otter as Theorem prover. I'm having some problems formalizing this: "John, Mary and Derek are three ...
6
votes
2answers
144 views

Is every proof for natural numbers equivalent to an induction proof?

The other day I had the following idea: Suppose one could show that a theorem for natural numbers is not provable by induction for all $n$, in other words, there do not exist useful induction steps ...
2
votes
0answers
90 views

How much arithmetic can Predicative Second-Order EFA do?

As discussed in this MathOverflow question, I'm trying to find what the result would be of applying a Feferman-Scutte-like analysis to the predicativism of Edward Nelson and Charles Parsons, who ...
2
votes
2answers
203 views

How can we define infinitary proofs?

In the first order logic the usual notion of a formal proof for a sentence $\sigma$ from a theory $T$ is a "finite" sequence ($<\omega$ - sequeance) of sentences which each one of them is a valid ...
0
votes
1answer
85 views

Can necessity rule be derived from box introduction rule?

I need to find a proof of $\top \vdash \Box \top$ (where $\top$ is the truth constant and $\Box$ is the necessity modal operator) in the natural deduction system of IS4 modal logic. In the axiomatic ...
3
votes
1answer
156 views

Type Theory (Proof tree)

Suppose $B(x)$ set $(x:A)$ is a family of sets and $D$ is a set. Prove $(\Sigma x:A)B(x) \times D \to (\Sigma x:A)(B(x) \times D)$. Using the so called Curry-Howard correspondence one may ...
3
votes
2answers
95 views

Proofs with Induction Imply Proofs Without Induction?

Assume we can prove $\forall x P(x)$ in first order Peano Arithmetic (PA) using induction and modus ponens. Does this mean we can prove $\forall x P(x)$ from the other axioms of PA without using ...
2
votes
3answers
126 views

Proof of $\exists x \exists y (\varphi(x)\rightarrow \psi(y)) \rightarrow \exists x (\varphi(x)\rightarrow \psi(x))$ in natural deduction

How to show the following trivial implication with natural deduction? $\exists x \exists y (\varphi(x)\rightarrow \psi(y)) \rightarrow \exists x (\varphi(x)\rightarrow \psi(x))$ Thx.
4
votes
1answer
160 views

Curry-Howard Correspondence (Proof Theory)

As you all know, the Curry-Howard correspondance provides a link between type theory and predicate logic. Concepts featured in the former, such as $\Pi$-type and $\Sigma$-type can, by the ...
1
vote
1answer
76 views

Given a theorem can it always be reduced logically to the axioms?

It's probably a silly question but I’ve been carrying this one since infancy so i might as well ask it already. let ($p \implies q$) be a theorem where $p$ is the hypotheses and $q$ is the ...
11
votes
2answers
514 views

Minimal difference between classical and intuitionistic sequent calculus

Consider propositional logic with primitive connectives $\{{\to},{\land},{\lor},{\bot}\}$. We view $\neg \varphi$ as an abbreviation of $\varphi\to\bot$ and $\varphi\leftrightarrow\psi$ as an ...
2
votes
1answer
125 views

Deduction Theorem Subtlety and Predicate Proof

In standard, first-order predicate logic suppose that with a set of assumptions $\Gamma$ I can deduce $$\Gamma\cup\{A(a),B(m),\forall x\forall y\exists z[A(x)\land B(y)\rightarrow C(x,y,z)]\}\vdash ...
0
votes
1answer
103 views

Unprovable unprovability of $\forall x\in X:P(x)$

Consider statements of the form $\forall x\in X:P(x)$. Is it possible that such a statement is proven to be unprovable? I think not, and here is my argument: if we proved that the statement is ...
2
votes
1answer
305 views

True and provably true sentences in a model. Are they the same thing?

In logic, it is said that each sentence in a (consistent) theory is either true or false in a given model. Checking the truth of a sentence in a finite model amounts essentially to finite enumeration ...
2
votes
1answer
169 views

Is the Church-Kleene Ordinal describable with Kleene's $O$?

Kleene's $O$ is an ordinal notation system that uses certain natural numbers to represent transfinite ordinals. It is a recursive notation system (although it's not decidable whether a number ...
4
votes
1answer
147 views

Is ordinal analysis a non-recursive project?

A recursive ordinal is an ordinal that is the order-type for some recursive relation (i.e. a recursive well-ordering). We can represent recursive ordinals as natural numbers using Kleene's $O$, an ...
5
votes
1answer
215 views

What is the proof-theoretic ordinal of the first-order theory of real closed fields?

I recently asked a question on MathOverflow, concerning a predicative second-order theory of real numbers. Now the standard way of developing predicativity in the case of second-order arithmetic is ...
1
vote
2answers
208 views

Simple proof theory - Propositional Logic

When addressing the questions, which are featured below, I use the following definition and two lemmas. Definition: $\phi$ is a tautology if $[[\phi]]_{v}=1$ for all valuations $v$. Moreover, ...
1
vote
1answer
139 views

Is the converse of the first Hilbert-Bernays Derivability Condition true?

The first Hilbert-Bernays Derivability Condition is (⊢P) → (⊢◻P). What I'd like to know is, is the converse true? That is, is (⊢◻P) → (⊢P) valid? I know from Löb's Theorem that ⊢(◻P → P) is not valid ...
4
votes
0answers
451 views

Difference between soundness and correctness

Is there any actual semantic difference between soundness and correctness? Can I use these words interchangeably when talking about formal reasoning, proof, logics, etc.? Otherwise, is there a ...
0
votes
3answers
566 views

Qns on Propositional Logic - Inference Rules + Logical Equivalence

Have been working on this for the past 2 hours and still not getting any where. Any help will be much appreciated! Consider the following argument 1) p 2) p v q 3) q → (r → s) 4) t → r ∴¬s → ¬t ...
5
votes
2answers
141 views

What is the meaning of proof of a proof?

After reading about Curry-Howard corrsepondence and looking at some proofs written in coq i've thinked about meaning of proof of a proof. We can express proofs as a computer program Proof is correct ...
-1
votes
1answer
107 views

Epistemic disjunction, axiom or rule?

Assume I have a minimal logic |- with disjunction v and implication ->. Now I want to represent some domain knowledge. One opponent says I should represent it as an axiom: ...
1
vote
1answer
93 views

Have I understood the whole Incompleteness business correctly?

I am reading Gödel-Escher-Bach and a good dialogue by Eliezer Yudkowsky and I think I might have understood the nature of the Completeness and Incompleteness theorems (at least regarding Peano ...
4
votes
2answers
155 views

How can arithmetic express claims of the form $\Sigma \vdash \sigma$ when $\Sigma$ is infinite?

As an example, let $\Sigma$ denote the axioms of ZFC (an infinite set). It is my understanding that the language of arithmetic can be used to express claims of the form $$\Sigma \vdash \sigma$$ where ...
7
votes
5answers
1k views

Books on logic, proof theory and set theory?

I graduated in Computer Science at University of Bologna in Italy some years ago. For various reasons now I am discovering a back interest in mathematic logic higher than I was a student. I have only ...
10
votes
2answers
565 views

Are the Gödel's incompleteness theorems valid for both classical and intuitionistic logic?

I am studying an undergraduate text about math logic. The proofs of the two Gödel's incompleteness theorems are not completely formal: they are admittedly simpler that the real proofs. For what I ...
1
vote
3answers
72 views

Show $s(s(a))=s(b)$ implies $s(a)=b$

Let us have a first order language $L=\{0,s\}$, where $0$ is a constant, $s$ is a function symbol of arity $1$. The first-order theory $T$ is axiomatized as follows: $\forall x \neg( s(x) = 0)$ ...
12
votes
1answer
262 views

Unprovable unprovability

In general, mathematical conjectures are resolved by proof, disproof, or proof that they are neither provable nor disprovable. Is it possible that some open conjectures cannot be settled in any of ...
8
votes
2answers
297 views

How is the standard model of number theory specified, and why can't we use that specification to prove any number theoretical sentence of interest?

According to Gödel's incompleteness theorem, there exists a sentence $G$ in the vocabulary of number theory ($N$) which is not provable from any (recursively enumerable) consistent set of axioms $T$, ...
2
votes
1answer
219 views

Different kinds of systems

I got interested in learning more about Logic, recently.The first thing i noticed is that this topic is a lot bigger than i expected. As i'm trying to make a sense of it all ( seeing the big picture ) ...
4
votes
1answer
190 views

Is the internal language of a topos complete, sound and effective?

The internal language of a topos is higher order intuitionistic typed logic. Now according to this article in wikipedia higher order classical logic with full semantics is never complete, sound or ...
13
votes
5answers
234 views

Does “=” have to be interpreted as equality?

To put it briefly: In model theory, we are allowed to interpret any relation symbol in any way we like. So why do people seem to require that "$=$" is interpreted as the actual equality? Let me ...
1
vote
2answers
648 views

Axiom Systems and Formal Systems

I'm a really beginner in Mathematical Logic.I'm currently reading Shoenfield Mathematical's Logic and i'm having a hard time trying to relate the concept of Formal Systems with the concept of Axiom ...
3
votes
1answer
97 views

Success of Hilbert's Axioms

We know Euclid's axioms were found to be having many loopholes as in there were still many assumptions which weren't being stated in his system of axioms . Are Hilbert's axioms today completely ...
9
votes
3answers
420 views

Prove by Hilbert deduction: $\vdash _{HFOL} \forall x (\neg(A \to \neg B))\to \neg(\forall xA \to \neg(\forall xB))$

I'd really like your help proving: $\vdash_{HFOL} \forall x (\neg(A \to \neg B))\to \neg(\forall xA \to \neg(\forall xB))$ Where $HFOL$ is the proof system which contains the Hilbert relevant ...
3
votes
2answers
254 views

Can the nonexistence of a constructive proof be proven when an existential proof exists?

Proofs are usually constructive or existential. For example, we know there are an infinite number of primes, and therefore the centillionth prime exists. We don't know what it is, though we can make ...
13
votes
8answers
4k views

Tricks for Constructing Hilbert-Style Proofs

Several times in my studies, I've come across Hilbert-style proof systems for various systems of logic, and when an author says, "Theorem: $\varphi$ is provable in system $\cal H$," or "Theorem: the ...
1
vote
1answer
317 views

Löb's theorem and provability

I learned Löb's theorem. As I understanding, if a statement is formed like "I am provable", the statement should be provable. I want to ask further about Löb's theorem. There is two sentences, P and ...
1
vote
0answers
92 views

proof checking machine vs. provability checking machine

Let M be a proof-checking Turing machine which takes two inputs, A and B. : M(A,B) = 0 if A codes a valid proof of the sentence coded by B in ZFC. M(A,B) = 1 if A does not code a valid proof of the ...
3
votes
1answer
120 views

What is the difference between $Γ⊭Φ$ and $Γ⊭¬Φ$?

Did I understand this correctly? $Γ⊨Φ$ ($Φ$ is considered true) $Γ⊨¬Φ$ ($Φ$ is considered false) $Γ⊭Φ$ ($Φ$ is considered neither true nor false) $Γ⊭¬Φ$ ??? Please help me understand. How can ...
1
vote
0answers
84 views

Examining every mathematical result in purely formal, ZFC language.

My main interest is physics. However, being self-taught in mathematics for the most part, my proofs tend to be more intuitive than it is acceptable. Yet, I recognize my inaptitude in rigor, and I ...
6
votes
1answer
183 views

Is there a useful Galois connection between Languages and Grammars?

I've just beginning to learn logic and proof theory - and the following rather vague and perhaps ill-formed question occurred to me. Given an alphabet it's straightforward to construct the Language, ...
12
votes
3answers
656 views

Gentzen Cut elimination: Why do we have to “go infinite”?

I found some slides here that say you can't do cut elimination on PA with axioms like $$\frac{P(Z)\;\;\;\;\;\forall n,\,P(n) \implies P(Sn)}{\forall n,\,P(n)}$$ (which denotes infinitely many axioms ...
6
votes
1answer
234 views

First order logic - how to prove a specific part of the completeness theorem?

I am working with the proof system for FOL described in Chang and Keisler. It contains the following axiom schemes: $\alpha \to (\beta \to \alpha)$ ...
2
votes
2answers
231 views

How can we know arithmetical axioms are consistent?

If we assume both distributivity and the opposite of the law of signs (ie, that $-1\times-1 = -1$) for the relative integers, then we can derive that two different numbers are actually equal. ...
2
votes
1answer
170 views

A pedantic question about defining new structures in a path-independent way.

Sometimes there are multiple equivalent ways of defining the same structure; for example, topological spaces are determined by their open sets, but also by their closed sets. I'm looking for a way of ...
7
votes
1answer
251 views

What are the formal properties of Godel numbering that are required to make it 'work'?

Godel numbering assigns a number to every formula. It appears to me that any encoding will do. However its also apparent, though I'm not sure how, that certain properties of the encoding used in Godel ...
1
vote
2answers
84 views

The standard approach to second-order axiom systems

This is a very basic question, but for some reason I couldn't find an answer elsewhere on the Internet. Suppose we have an axiom system $A$ written in the language of second-order logic. In order to ...