Questions tagged [proof-theory]
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-* ...
2
votes
1answer
70 views
Can meta-languages disagree over what an object language proves?
Suppose we have a language/theory $\mathcal{L}$ in First Order Logic, and we look at what it proves. Is it possible that there are two meta-languages/theories, say $\mathcal{L_1}$ and $\mathcal{L_2}$, ...
2
votes
0answers
53 views
How can any proof of Gödel's incompleteness theorem be accepted considering systems of mathematics themselves are incomplete?
I believe there are at least several proofs of Gödel's incompleteness theorem. Nagel and Newman wrote a book (1958) that presents one in particular.
But considering the theorem itself exposes ...
0
votes
0answers
28 views
McNaughton functions and hypersequents for Lukasiewicz logic
For this question, all definitions are borrowed from Proof theory for fuzzy logics (2008) by Metcalfe, Olivetti, and Gabbay.
Consider a propositional language over $\{\rightarrow,\bot\}$ for infinite ...
1
vote
1answer
43 views
Is this proof of $(S \cap T)^c=S^c \cup T^c$ valid?
I'm self-learning set theory, and as an exercise, I tried to prove one of DeMorgan's laws, i.e.,
$$(S \cap T)^c=S^c \cup T^c$$
So my proof goes as follows:
Let $x \in S^c$, and $x \in T^c$. Then,...
-1
votes
0answers
21 views
Question about proposition from P. Fletcher 1.10
I have been trying to solve the case below about propositions but did not a find a right approach to answer this. I started with creating two propositions: A and B which state that (A) Tech will beat ...
1
vote
2answers
66 views
Does natural deduction require a non-empty set of premises?
Normally in a Hilbert system, writing a proof $\Delta \vdash \varphi_n$ with lines $\varphi_1, \varphi_2, ..., \varphi_n$ is done such that each $\varphi_k$ is either a proposition contained in $\...
2
votes
1answer
37 views
Proving soundness property of a Hilbert system
Now that I have a better understanding of soundness, I'd like to try this again.
My goal is to prove that the classical Hilbert system has the soundness property:
$$\Gamma \vdash \varphi \implies \...
-1
votes
1answer
44 views
Proof that this is a a subspace [closed]
My math is really getting rusty, I need some help on the following problem.
Proof that
$y$ in $R^n$: $y = Xk$, where k in $R^m$, this is subspace of $R^m$
Is this in $R^m$ by default?
1
vote
0answers
37 views
Prove $\Sigma \vdash \lnot(\phi \rightarrow \psi)$ iff $\Sigma \vdash \phi$ and $\Sigma \vdash \lnot \psi.$
$\Sigma$ is a set of sentences, the set $ L$ consists of all axioms of the forms:
A1)
$ \ \phi \rightarrow (\psi \rightarrow \phi)$
A2) $\ (\phi \rightarrow (\psi \rightarrow \theta)) \rightarrow (...
-1
votes
1answer
42 views
Proof-mathematical induction
n > 0 red balls and n blue balls are arranged to form a circle. You walk around the circle
exactly once in a clockwise direction and count the number of red and blue balls you pass.
If at all times ...
2
votes
2answers
125 views
Why and how is logic related to set theory?
I am learning set theory on my own at the moment, and I realised I can't avoid not to learn logics. There is a strong connection between these two. such that, proofs for sets are based on logics.
I ...
1
vote
1answer
52 views
Assumptions necessary to justify the method of proof by contradiction.
It seems to me, these assumptions are necessary to demonstrate proof by contradiction:
i) Every proposition must belong to $T$ or $F$.
ii) No proposition belongs to both $T$ and $F$
iii) If having $...
-2
votes
2answers
102 views
Does Gödel's incompleteness theorem invoke a Law of Excluded Middle contradiction? [closed]
Does Gödel's incompleteness theorem cause the Law of Non Contradiction to contradict its self?
If so, would this be a considered a conjecture?
1
vote
1answer
143 views
Proving the distributive law with natural deduction
I have to prove the following logical equivalence, also known as one of the two distributive laws:
$$
P \vee (Q \wedge R) \equiv (P \vee Q) \wedge (P \vee R)
$$
I have solved the first part, $P \lor ...
1
vote
0answers
28 views
Intersection graph of sub-tree is an interval graph
$\Gamma$ be a set of subtrees of a tree T.
Let G(V,E) is a interval graph if $\ni I$ of intervals {$i_1, i_2 ... i_n$}
$f: V \rightarrow I $ such that $f(v_i)$ and $f(v_j)$ intersect.
...
1
vote
2answers
73 views
Stuck on a beginner proof writing: Prove: If U = A ∪ B and A ∩ B = ∅ then A = U \ B.
While I was trying to work on the proof, I realized I never ended up using the second given, A ∩ B = ∅. Then I realized my logic could be off entirely, but I'm not entirely too sure what about it ...
0
votes
2answers
20 views
How to define a addition and multiplication operators over a set R U {infinity} U {-infinity}?
And, are the sets {infinity} and {-infinity} actually infinite sequences in their respective directions, such that I could define the operators as such? :
= a(x1, ...) = (ax1, ax2, ...)
= (x1, ...) + ...
0
votes
0answers
58 views
Can we be sure proofs have no errors?
My current understanding is that work submitted to journals has mathematicians look over it for errors. Mathematics is deductive, yet with this being the burden of proof, how can we know for sure ...
2
votes
1answer
42 views
About proofs that we cannot verify every step by hand
For something I am planning to write, I need to clarify few issues with respect to computer-aided proofs that we cannot verify every step by hand. For example, the proof for the four-color map theorem....
1
vote
0answers
61 views
Is there software to validate formal demonstrations?
Anyone knows a software that compiles formally well-defined algebraic equations to validate their correctness?
For example, I insert a statemente in latex like that:
\forall S_i \in S \to \exists! ...
5
votes
3answers
161 views
Predicate Logic, Proof of validity . How to remove negation infront of existential quantifier?
$\forall x~(P(x) \to (Q(x) \lor R(x))), \lnot \exists x~(P(x) \land R(x)) \vdash \forall x~(P(x) \to Q(x))$
I am stuck on how to get rid of the negation on "$\lnot \exists x~(P(x) \land R(x))$" in ...
3
votes
1answer
67 views
Is this proof for if $0 < a < b$ then $a^2 < b^2$ correct?
I'm reading the book 'How to prove it' from Daniel Velleman which he presents a proof for the following; if $0 < a < b$ then $a^2 < b^2$ as;
Proof. Suppose $0 < a < b$. Multiplying ...
2
votes
1answer
39 views
Determining whether proofs of the Pythagorean theorem are essentially the same, or essentially different
There are great annotated lists of proofs of the Pythagorean theorem, to name just two:
cut-the-knot.org
brilliant.org
There's an obvious difference between geometric and algebraic proofs (which ...
6
votes
3answers
913 views
George Boolos and Gödel's Second Incompleteness Theorem
In Mind, Vol. 103, January 1994, pp. 1-3, George Boolos wrote:
And so on. In fact, if a claim can be proved, then it can be proved
that the claim can be proved. And that too can be proved.
...
2
votes
1answer
47 views
Equivalence in Natural deduction in First-order logic 2
I would want to check with you guys if I've done the following natural deduction correct. The reason being that I haven't gotten any answer sheet for this task.
Task
Solve the following with natural ...
2
votes
3answers
59 views
Equivalence in natural deduction in First-order logic
Task
$\vdash \exists x (P(x)\lor Q(x)) \iff \exists xP(x) \lor \exists xQ(x) $
My answer
If we have $A \iff B$ then $A\vdash B$ and $B \vdash A$.
So I started trying to see if I could prove $B$ ...
2
votes
1answer
49 views
Natural deduction in first-order logic
I've sat for more than an hour now and I don't understand how I'm supposed to solve the task below.
$\{\forall x(P(x) \land Q(x)), \exists x\neg P(x)\} \vdash \exists x \neg Q(x) $
So I'm a bit ...
5
votes
1answer
125 views
Is Fermat's last theorem provable in Peano arithmetic?
The sentence $S$ which Gödel in his proof of the incompleteness theorem proves to be be unprovable in the system of Peano arithmetic can be proved (as a true theorem of PA) outside PA (and necessarily ...
1
vote
2answers
56 views
Soundness of cut in Gentzen's System LK
I'm learning the sequent calculus in the classical setting (Gentzen's System LK), and I am a little confused about how to understand the soundness of Cut.
As I understand it, for a given sequent, we ...
-1
votes
1answer
73 views
Can all proven theorems be proven by contradiction?
The answers to the question Can every true theorem that has a proof be proven by contradiction? show that if a theorem can be proven directly, it can be proven by contradiction.
The main arguments ...
-3
votes
1answer
54 views
Is there a statement which can not be proved in any axiom systems
As we know a statement may not be proved in some axiom system according to the godel incompleteness theory, can we always solve it by some way that change the axiom system?
2
votes
1answer
132 views
Translating from First Order Logic to Order-Sorted Logic
The following single sorted FOL sentences are from Stanford. Sorts or types are represented by predicates (e.g. $Horse(x)$)
\begin{align*}
&(1a) \forall x, \forall y ((Horse(x) \land Dog(y)) \...
2
votes
1answer
70 views
Exercise 2 (p. 30) on W. Rautenberg - A concise introduction to Logic.
I'm can't solve Exercise 2 on page 30 on Rautenberg (Chapter 1.4 - A calculus of Natural Deduction), which reads:
Augment the signature $\{\lnot, \land\}$ by $\lor$ and prove the completeness of the ...
2
votes
2answers
112 views
Doubts about Goedel Completeness Theorem
My book (Mendelson) states this theorem the following way:
(1) A logically valid formula of a first order theory is a theorem.
On Wikipedia the statement is a little more general:
(2) For any ...
2
votes
1answer
196 views
About proofs by contrapositive and proofs by contradiction
I'm a little confused about the difference between these two types of proof. As I have been taught them, it seems like proofs by contrapositive are just a subset of proofs by contradiction.
Say we ...
0
votes
2answers
41 views
Induction proof inequality
So I got this induction proof question but I can't seem to make a logical statement in one part of it:
The question is , $a_{n + 1} = 5 - \frac{6}{a_n + 2}$ with
$a_1 = 1$ . Prove by induction that ...
22
votes
10answers
3k views
What exactly is circular reasoning?
The way I used to be getting it was that circular reasoning occurs when a proof contains its thesis within its assumptions. Then, everything such a proof "proves" is that this particular statement ...
1
vote
1answer
53 views
Independence and Consistence of Formal Systems
Let $S$ be a formal system with axioms $A,A_1,\dots,A_n$. The system $S$ is said to be consistent if no contradiction can be proved (i.e. we can’t prove both a formula and its negation). If $S$ is ...
4
votes
2answers
174 views
Curry-Howard for an imperative programming language?
The Curry-Howard isomorphism links proofs of propositions, with "programs" and types.
But the way I am introduced to it, "programs" is interpreted in a functional way, i.e. in lambda calculus with ...
5
votes
1answer
117 views
Why can't we generally replace inference rules with axioms?
Is there a big difference in having insufficient axioms and insufficient inference rules/proof procedure to have a complete theory?
It seems like in many cases adding a new inference rule or a new ...
2
votes
0answers
78 views
Paradox,shortest proof
I have read somewhere that the shortest proof of a certain formula in the language of natural numbers contains some kind of paradox. I cannot remember what this paradox was nor where I've read it. It ...
2
votes
1answer
26 views
sequent calculus for first order logic
I've just started learning sequent calculus. Now I'm trying to prove the formula below:
$$ \exists x (P → Q) ⊨ P → \forall x Q $$
My approach to the problem:
$$ \underline{_⊢\exists x (P → Q) , _⊣ P ...
1
vote
2answers
144 views
Axioms of propositional logic
The book on which I'm studying logic (Mendelson) uses the following axioms:
$$\begin{array} {rl}
\text{A1)} & P \to (Q \to P) \\
\text{A2)} & [P \to (Q \to R)] \to [(P \to Q) \to (P \to R)...
0
votes
1answer
65 views
What does this proof mean?
I'm having difficulty reading these proofs,
Definition 1 $V$ is an NP-verifier for $L$ if $V$ is polynomial-time in the length of the first input and that the following two properties hold:
...
1
vote
2answers
52 views
universal instantiation and the Archimedean property
I have been under the impression that I could substitute just about anything for the variables in any proven theorem (via universal instantiation logic rule) but when applied to the Archimedean ...
1
vote
0answers
50 views
Fitch-style Deductive Proof
I am having trouble with the following question:
Give natural deduction proofs of the following formulas (from no assumptions):
$p \to p$.
Here is what I have so far:
$$\begin{array}{|l}\hline~~\...
0
votes
0answers
19 views
When are (hyper)cubes used instead of balls as the basic constructs to argue for “whole” spaces?
When are (hyper)cubes used instead of balls as the basic constructs to argue for "whole" spaces?
Like e.g. when one wants to prove smoothness properties through induction (prove for unit ball $\...
5
votes
3answers
543 views
Defining new symbols in a proof, when is this justified?
So I have a proof that I have written of $X\subset Y \Rightarrow f(X)\subset f(Y)$ but it is slightly different than the one presented in this questions accepted answer.
The difference is subtle so ...
2
votes
1answer
48 views
Proof theory outside of structural proof theory (calculi)?
Is there proof theory for some more or less usual logics that is outside the scope of structural proof theory (Hilbert/natural deduction/sequent calculi)? E.g. proof theoy for adaptive logic (https://...
4
votes
3answers
132 views
Is there a type of mathematical proof besides direct, counterpositive and absurd?
When proving a mathematical statement $p \Rightarrow q$, we normally do it:
1) Assuming $p$, then showing $p \Rightarrow q$ (Direct proof)
2) Assuming $¬q$, then showing $¬q \Rightarrow ¬p$. (...
