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

12
votes
1answer
228 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 ...
7
votes
2answers
241 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
197 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
166 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
230 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
469 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
91 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
389 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 ...
47
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
224 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 ...
12
votes
8answers
3k 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
587 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
161 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
302 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
88 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
104 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
63 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
79 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
169 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
580 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
207 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
204 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
160 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
225 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 ...
4
votes
2answers
152 views

Currying and Uncurrying of logical formulas, is $(A \land B) \to C \leftrightarrow (A\to B)\to C$

With a truth table its easy to see that the two formulae $A\land B \to C$ and $A \to B \to C$ are not equivalent, for example, if $A = B = C = 0$, than the first evaluates to $1$ and the second to $0$ ...
2
votes
2answers
109 views

Want to show the a proof of the sequent $\forall x \forall y R(x,y) \Rightarrow R(y,y)$ must have a cut

Want to show the a proof of the sequent $\forall x \forall y R(x,y) \Rightarrow R(y,y)$ must have a cut. For this question we are in the Gentzen calculus. I am even having trouble just finding a ...
4
votes
2answers
257 views

Sequent calculus and first incompletness theorem

Wikipedia says that sequent calculus is sound and complete (http://en.wikipedia.org/wiki/Sequent_calculus#Properties_of_the_system_LK). Godel first incompleteness theorem says that system capable of ...
46
votes
2answers
1k views

Is it possible to prove a mathematical statement by proving that a proof exists?

I'm sure there are easy ways of proving things using, well... any other method besides this! But still, I'm curious to know whether it would be acceptable/if it has been done before?
13
votes
7answers
2k views

Is a counterexample considered a rigorous proof that a property is not true?

This is my follow-up question to my own query earlier: How can I algebraically prove that $2^n - 1$ is not always prime? Almost half of the answers said that I provided my own proof by giving ...
3
votes
2answers
241 views

Goodstein's theorem without transfinite induction

Is it possible to prove Goodstein's theorem without transfinite induction? Is there such a proof?
5
votes
1answer
1k views

Why can't reachability be expressed in first order logic?

I'm wondering why we can't express graph reachability in first order logic in pretty much exactly the same way we express it in second order existential logic. For SOL, one definition is : 1 . L is ...
4
votes
1answer
94 views

Proofs whose length depends on the input

This may be a question from proof theory, but I'm not sure, since I don't know any proof theory. What I will be asking about is what happens, if the length of a proof isn't fixed: I'm going to present ...
191
votes
14answers
8k views

Can every proof by contradiction also be shown without contradiction?

Are there some proofs that can only be shown by contradiction or can everything that can be shown by contradiction also be shown without contradiction? What are the advantage/disadvantages of proving ...
1
vote
1answer
455 views

proof of validity of tautology in first order logic

Every first-order logic formula which has a tautological shape in propositional logic is a valid formula. Will it be possible to give a formal proof for the above ? Thanks and Regards.
7
votes
1answer
207 views

Are coinductive proofs necessary?

I've been exploring corecursion in Coq (specifically, infinite streams of natural numbers) lately and so far any coinductive predicate I've constructed and its coinductive proof can be transformed ...
0
votes
2answers
218 views

is it possible to prove the method of mathematical induction itself?

Since the method of mathematical induction follows some sort of 'algorithm', would the method itself be provable? namely, give that the method of mathematical induction is as follows: if S is a ...
2
votes
1answer
231 views

Proof the following proposition: for all $n \geq 0, \mathrm{fib}(n) \leq n!$

I am a comp science undergrad and just started to learn proof. And I have been thinking about this question for a few days. How should I present my answer? Do I have to use the Binet's formula? Or can ...
17
votes
5answers
1k views

If it takes infinite steps to prove a statement, is that a valid proof?

In Cantor's diagonal argument, it takes (countable) infinite steps to construct a number that is different from any numbers in a countable infinite sequence, so in fact the proof takes infinite steps ...
1
vote
2answers
143 views

Is a valuation of a logic formula always a trivial task? I.e. is it practically executable?

For a given structure for a quantified theory, is the valuation of any formula always practically executable? In the case of propositional calculus, where every formula has a certain degree, ...
2
votes
1answer
149 views

Sequent calculus - proofs as trees or sequences

First at all, I am new at proof theory, so excuse this perhaps redundant question. I am wondering what is the 'most appropriate' definition of a proof in a sequent calculus (e.g. LK). Proofs as trees ...
5
votes
3answers
665 views

Is the negation of the Gödel sentence always unprovable too?

The incompleteness theorem says that certain theories+deduction system contain at least one sentence (the Gödel sentence "$G$"), which can't be proven (in the system in which it holds). (i) Is ...
4
votes
3answers
466 views

What do we mean by an “Elegant Proof”? [closed]

What do we mean when we say that a mathematical proof is elegant? Of course one can say that the proof is beautiful, but what do we precisely mean when we say that a proof is beautiful ? Is there a ...
7
votes
1answer
151 views

Learning how to prove that a function can't proved total?

In proof-theory one can prove that in, say, Peano Arithmetic one can't prove a function $f$ total. Often this seems to mean $f$ is growing too fast to be provably total. I have some background in ...
5
votes
3answers
392 views

Aftermath of the incompletness theorem proof

This is somewhat of a minor point about the incompletness theorem, but I'm always a little unsure: So one proves that there is a formula which is unprovable in the theory of consideration. Okay, at ...
5
votes
5answers
368 views

Can we decide a conjecture is decidable without knowing a conjecture is correct or false?

Can we decide a conjecture is decidable without knowing a conjecture is correct or false? I asked this question because I assume that the millenium prize problem is already to be decidable, otherwise ...
4
votes
3answers
309 views

Impossibility of certain methods of proof?

There are many methods available for proving a given statement: direct proof, proof by induction, proof by contrapositive, proof by contradiction, etc. In some cases there is an obvious method that ...
3
votes
3answers
475 views

Statements true for all integers but not provable by induction

Is there any examples of statements P(n) such that "for all $n>1$, P(n)" is provable, but P(n)=>P(n+1) is not provable? (without using some mild deformation of "for all $n>1$, ...
3
votes
1answer
154 views

Lengths of proof

Let $f(n)$ be the length of the shortest statement whose shortest proof has length $n$ or more. What are the asymptotics of $f(n)$? With standard symbols and length counted by character. For any ...
4
votes
4answers
595 views

What is the difference between ⊢ and ⊨?

I want to know the difference between ⊢ and ⊨. http://en.wikipedia.org/wiki/List_of_logic_symbols ⊢ means ”provable” But ⊨ is used exactly the same: ...