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
128 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
201 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
108 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
65 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
443 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
197 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
180 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
180 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
75 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
119 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
185 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
238 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
329 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
183 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
371 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
139 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
264 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
77 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
90 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
71 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
143 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
422 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
175 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
182 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
141 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
190 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
80 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
124 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
88 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
193 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 ...
38
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
1k 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
205 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
676 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
91 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 ...
140
votes
13answers
6k 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
330 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
190 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
171 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 ...
-1
votes
1answer
121 views

Stuck on proving demorgans with quantifiers

What I'm trying to prove, using propositional and quantifier rules, is $$\neg \exists{x} \; A(x) \iff \forall{x} \; \neg A(x).$$ So far, I've only started proving it left to the right, and I'm ...
2
votes
1answer
218 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
130 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, ...