Proof theory is an area of logic that studies proof as formal mathematical objects. For questions asking how to write proofs or for checking an informal proof, please use the proof-writing or proof-strategy tags instead.

learn more… | top users | synonyms

2
votes
0answers
53 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
113 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
66 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
109 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 ...
2
votes
2answers
76 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 ...
4
votes
1answer
115 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 ...
2
votes
1answer
67 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 ...
8
votes
2answers
246 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
85 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 ...
15
votes
2answers
235 views

How much math do we need to prove all simple numeric identities?

Consider real numeric expressions build only from integers, operators $+,-,\times,/$ and taking a positive expression to a power (no variables involved), e.g. $$\frac{2}{7},\ 2^{1/2},\ ...
0
votes
1answer
85 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
174 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
94 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
74 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
146 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
140 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
82 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 ...
2
votes
0answers
138 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
206 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
1answer
112 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
69 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
81 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
152 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 ...
4
votes
5answers
500 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 ...
6
votes
1answer
206 views

Are the Godel's incompleteness theorems valid for both classical and intuitionistic logic?

I am studying an undergraduate text about math logic. The proofs of the two Godel'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)$ ...
11
votes
1answer
186 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 ...
6
votes
2answers
185 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
84 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
123 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 ...
12
votes
4answers
186 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
272 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
83 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
335 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 ...
43
votes
13answers
3k views

What is a proof?

I am just a high school student, and I haven't seen much in mathematics (calculus and abstract algebra). Mathematics is a system of axioms which you choose yourself for a set of undefined entities, ...
3
votes
2answers
186 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 ...
7
votes
8answers
2k 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 ...
2
votes
2answers
379 views

question about vacuous proof

Hi i have a question about vacuous true and it always make me confused~ if I want to proof empty set is the subset of all the set A, the proof is as following: if x is in empty set, then x is in A. ...
3
votes
5answers
156 views

Is there Problem with an Answer that can't be found?

I have been thinking about something and I don't know whether it's possible or a contradiction, 't is as follows: Is there a mathematical problem for which we know there is an actual answer, but for ...
1
vote
1answer
268 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
78 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 ...
2
votes
1answer
93 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
58 views

Direct Proof and Proof by Contradiction [duplicate]

This might seem like a random question but I am wondering can every theorem that can be proved through contradiction be proved directly or vice versa, that is is one a subset of the other or is there ...
1
vote
0answers
72 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
147 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, ...
11
votes
3answers
436 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 ...
5
votes
1answer
180 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)$ ...
1
vote
2answers
188 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
144 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 ...
6
votes
1answer
194 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 ...