Tagged Questions
2
votes
1answer
53 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 ...
4
votes
1answer
99 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
108 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. ...
2
votes
4answers
98 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 ...
0
votes
1answer
118 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
61 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 ...
37
votes
13answers
3k views
Is there such a thing as proof by example (not counter example)
Is there such a logical thing as proof by example?
I know many times when I am working with algebraic manipulations, I do quick tests to see if I remembered the formula right.
This works and is ...
2
votes
1answer
67 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
31 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 ...
5
votes
2answers
121 views
What quantifies as a rigorous proof?
Okay I have been thinking about this common combinatorial identity. $$\sum_{r=0}^{n} \binom{n}{r} = 2^n.$$ It is simple to prove this by induction, but it requires some annoying algebraic manipulation ...
6
votes
0answers
85 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, ...
8
votes
2answers
174 views
Ordinal interpretation of Friedman's $n$?
I heard that Kruskal's tree theorem can be turned into a finite form that creates an extremely fast growing function because ordinals could be encoded into trees.
On this wiki page it mentions that ...
10
votes
2answers
195 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
86 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
107 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.
...
6
votes
1answer
115 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
67 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 ...
3
votes
2answers
79 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$ ...
1
vote
0answers
44 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
115 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 ...
34
votes
2answers
671 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?
24
votes
2answers
819 views
Proof by contradiction vs Prove the contrapositive
What is the difference between a "proof by contradiction" and "proving the contrapositive"? Intuitive, it feels like doing the exact same thing. And when I compare an exercise, one person proofs by ...
3
votes
2answers
127 views
Goodstein's theorem without transfinite induction
Is it possible to prove Goodstein's theorem without transfinite induction? Is there such a proof?
1
vote
1answer
237 views
Strong induction proofs
I'm having trouble understanding strong induction proofs
I understand how to do ordinary induction proofs and I understand that strong induction proofs are the same as ordinary with the exception ...
3
votes
1answer
175 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
69 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 ...
0
votes
1answer
45 views
Verify these logical equivalences by writing an equivalence proof?
I have two parts to this question - I need to verify each of the following by writing an equivalence proof:
$p \to (q \land r) \equiv (p \to q) \land (p \to r)$
$(p \to q) \land (p \lor q) \equiv q$
...
0
votes
1answer
63 views
Prove/disprove this logical equivalence using basic equivalences?
I need to prove/disprove the logical equivalences of the following statement using basic equivalences:
p→(q→r) and q→(p→r).
I can do everything apart from the proofs in my work :/
Thank you if you ...
0
votes
1answer
73 views
Need some help with some mathematical proofs (logical equivalences and normal proofs)
I need to prove/disprove the logical equivalences of the following two statements using basic equivalences:
$p \to (q \to r)$ and $(p \to q) \to r$.
$p \to (q \to r)$ and $q \to (p \to r)$.
I ...
109
votes
13answers
4k 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
0answers
163 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.
0
votes
1answer
74 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 ...
13
votes
5answers
811 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
103 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
86 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
299 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 ...
7
votes
1answer
114 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 ...
3
votes
3answers
251 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 ...
4
votes
3answers
246 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
193 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
129 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 ...
3
votes
4answers
307 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:
...
1
vote
1answer
228 views
Proving or disproving expression with implies operators
I'm having a hard time reducing expressions involving "implies" operators. I did some reading about the actual meaning of the "implies" operator and browse for other Q&A on this website; however, ...
6
votes
1answer
155 views
Consistency of PA: why other proofs?
Completeness theorem affirms that a formal first order system is consistent iff it has a model. The FOL number theory(PA) or First Order Arithmetic has a model, which is the natural numbers structure. ...
1
vote
1answer
161 views
subformula property (anchored proofs)
0
Hello,
I would like to ask for some explanation on some property of propositional sequent calculus. The sequent calculus that I use here follows that of Stephen Cook, in "Logical Foundations of ...
4
votes
2answers
176 views
Are all proofs “short enough” to be computed?
The Completness Theorem in Propositional Logic says that a tautological statement has a derivation.
Does this existence imply that this derivation consists of a finite formation sequence?
I ...
4
votes
1answer
142 views
Formal proof involving $\varphi( v_k / v_l )$
I'd like to show that if $\varphi(v_k / v_l )$ and $\varphi(v_l / v_k )$ are admissible then $[\exists v_k \varphi(v_k)] = [\exists v_l \varphi(v_l)]$ where $[\varphi]$ denotes the equivalence class ...
1
vote
2answers
302 views
Contradiction Theorem
I'm a beginner in formal logic. Can anyone of you help me with the proof of the following lemma:
For any Theory $T$ and closed formula $\varphi$ it holds that $T \vdash \varphi$ if and only if ...
5
votes
2answers
533 views
Definition of “non-constructive proof”
I was wondering if it is possible to define exactly what a non-constructive (nc) proof is. I have often seen the concept associated with the use of principles such as the axiom of choice or the law of ...
3
votes
1answer
112 views
What is a relatively bound variable?
edit: Interestingly, the authors also state at one point that the choice of introduction rule is determined by the structure of the previous goal and the list of introduction rules; but at another ...
