1
vote
2answers
130 views

Mathematical statements that cannot be proved or disproved [on hold]

I've recently been reading about the continuum hypothesis and am fascinated by the fact that it cannot be proved or disproved, despite the fact that the statement itself is either true or false. What ...
2
votes
0answers
62 views

Can we always give a direct proof? [duplicate]

This is something I was wondering about for quite a while. Is it possible to construct a statement that can only be proven by using 'proof by contradicition' or contraposition? Or to put it ...
7
votes
1answer
150 views

Gödel's way of teaching non-standard models to Takeuti.

In Memoirs of a Proof Theorist, Gaisi Takeuti relates how Gödel taught him about nonstandard models in an "interesting" way: It went as follows. Let T be a theory with a nonstandard model. By ...
0
votes
1answer
56 views

particular property and completeness?

I was puzzeling with the almost standard definition of completeness: In mathematical logic and metalogic, a formal system is called complete with respect to a particular property if every formula ...
1
vote
3answers
89 views

Defining a partial function in a formal theory

Assume we have a first-order theory $T$ of arithmetic (i.e., number theory). Suppose I wish to introduce a new function symbol $f$ in the theory, so that $f$ is a partial number function (namely, it ...
1
vote
3answers
76 views

$\neg(A\Rightarrow B) \iff A\land \neg B$

When considering the question: Rewrite the following using only the symbols $A, B, \lor, \land, \neg$ : $$\neg(A\Rightarrow B)$$ I do not understand how to interpret this and what method to ...
3
votes
1answer
36 views

$HA^{\omega}$ is a conservative extension of $HA$. But why?

This is definitely a silly question, but I've no one to ask... $HA^{\omega}$ is an extension of $HA$ in all finite types. One can formalize a model of $HA^{\omega}$ in $HA$ using indicies of partial ...
3
votes
5answers
86 views

Difference between bound and free variable

What is the difference between $\forall x (P(x)\implies Q(x))$ and $P(x)\implies Q(x)$ I know in the first one the variable x is bound but in the second one the variable is free. What are the ...
0
votes
1answer
123 views

Formal proofs and Deduction Theorem

In this question i will explain one idea i had about basic formal proofs and the use of Deduction Theorem. I'm considering a formula γ to be a logical consequence of a set A of formulas if and only ...
3
votes
2answers
89 views

Law of excluded middle. Do we need it in proofs?

Quite often when I am making a natural deduction proof, and I have no fixed idea on how to continue. I find myself thinking: "lets start with some form of the law of the excluded middle (LEM) and ...
4
votes
2answers
76 views

Graph that represents logical reasoning

The proof of a statement $X$ in terms of assumptions $A$, $B$ and $C$ can sometimes be represented using a directed graph: $$ \begin{matrix} & & X\\ & \nearrow & & ...
9
votes
1answer
142 views

Can all math results be formalized and checked by a computer?

Can all math results, that have been correctly proven so far, be formalized and checked by a computer? If so, what type of logic would need to be used there? I've heard that the first-order logic is ...
3
votes
2answers
122 views

General view of Theorems

I'm trying to see almost all theorems ( at least the non-existential ones ) as affirming that some formula ( mostly of first-order logic language ) is a logical consequence of other formulas. So, ...
0
votes
1answer
64 views

Hilbert calculus: Proof that every provable formula has a proof

For my indroduction to logic course I have to proof, that every provable formula has a proof. It sounds first very funny, second also very logic, still I don't get to make of formally work.. The ...
0
votes
1answer
32 views

Proving that operations give equal results given equal inputs

I was reading about the 9 or 12 basic properties of 'fields' (if that's what they're called) in a book called Spivak's Calculus, 3rd Edition, and got quite befuddled by dealing with as basic stuff as ...
2
votes
1answer
42 views

$LK-\Phi$ proof of $\exists y Pby$

I am having difficulty with the concept of $LK-\Phi$ proofs, here is a question I have been working on: Let $\Phi = \{Pafa\}$, where $P$ is a binary predicate symbol and $f$ is a unary function ...
1
vote
3answers
138 views

ZFC Axioms to be extended?

Sorry if this is going to be a really loaded question. I was told several times that for virtually all theorems/corollaries/propositions of mathematics (except those cases not compatible with ZFC ...
2
votes
1answer
120 views

Provable formulas in everyday Mathematics

Basically all statements ( lemmas, theoremas, corollaries ) in Mathematics can be expressed as a conditional statement in first-order language, or existential statement ( existence proofs ). Here ...
3
votes
2answers
102 views

Model-theory and Proof-theory in Propositional Logic

I'm trying to link results of model theory and proof-theory in propositional language. Here i will use $\models$ to denote logical consequence, in the model-theory sense. Being $x,y$ two formulas of ...
1
vote
1answer
34 views

The approximation rule implies the equality rule in systems of type assignments

I'm reading Barendregt's Lambda calculi with types (1992). In Proposition 4.1.4.1., he "proves" a lemma which shows the approximation rule implies the equality rule in typed lambda-calculi à la ...
47
votes
8answers
5k views

Is it possible that “A counter-example exists but it cannot be found”

Then otherwise the sentence "It is not possible for someone to find a counter-example" would be a proof. I mean, are there some hypotheses that are false but the counter-example is somewhere we ...
1
vote
2answers
81 views

Does generalization of axioms apply also to theorems?

In Enderton's book "A Mathematical Introduction to Logic" (second edition), he includes six axiom groups, and allows also for a generalization of those axioms such that if $\Psi$ is an axiom then ...
3
votes
1answer
65 views

Intuitionistic Linear Logic

I am currently going through some papers that use the "intuitionistic version" of Girard's Linear Logic. Problem is, i seem to find very little literature on it. There is a lot done on Linear Logic ...
3
votes
2answers
61 views

Double Negation is sequent calculus systems LK and LJ

In sequent calculus LK (see Gaisi Takeuti, Proof Theory (2nd ed - 1987)) we have a "standard" derivation of Double Negation in the form $\rightarrow \lnot \lnot A \supset A$. We have to start from an ...
2
votes
1answer
62 views

Proof negation in Gentzen system

I am provided with the L¬ and R¬ Gentzen rules for negation (besides “Cut” rule and some rules for ⋀ and →): $${\Gamma\vdash\Delta,\varphi\over \Gamma,\lnot\varphi\vdash \Delta}\ L\lnot \\[4ex] ...
1
vote
1answer
66 views

If $\phi$ is $\Delta^{0}_{1}$ in the language of arithmetic, does Heyting Arithmetic prove $\forall x [\phi (x) \vee \neg \phi (x)]$?

PA is conservative over HA for $\Pi^{0}_{2}$ sentences. If $\phi$ is $\Delta^{0}_{1}$, then $\forall x [\phi (x) \vee \neg \phi (x)]$ is equivalent to a $\Pi^{0}_{2}$ sentence. Since PA trivially ...
2
votes
1answer
51 views

Does second-order arithmetic (Z2) prove soundness and uniform reflection for first-order arithmetic (PA)?

(1) Does full second-order arithmetic (Z2) prove soundness and uniform reflection schemas for first-order arithmetic (PA)? That is, do we have for all formulas $\phi$: $$ \underset \phi \forall \; ...
4
votes
1answer
138 views

What are those “things that cannot be proved using only ordinary rules of inference”?

The online edition of the book Introduction to Logic by Michael Genesereth and Eric Kao, has a detail that left me confused. CHAPTER 4 [...] 4.2 Linear Proofs [...] The ...
6
votes
3answers
220 views

Give a proof that “p & ~p” implies “q”?

Context: This is not a textbook or homework problem. I was hoping you younger folks could help my tired old brain. "Everybody knows" a contradiction implies anything. What I'm looking for is a ...
0
votes
1answer
51 views

Help with positive- and negative-forms in Proof Theory

I need help in understanding a device used bu Kurt Schütte, Proof Theory (1977). In treating classical sentential calculus, he use - in place of truth-tables - the device of positive- and ...
2
votes
2answers
94 views

Proof for $\{p,p\rightarrow (q\rightarrow r)\}\vdash (p\rightarrow q)\rightarrow r$ in HR

I can't find a for $\{p,p\rightarrow (q\rightarrow r)\}\vdash (p\rightarrow q)\rightarrow r$ in HR HR is the following system: axioms: $A\rightarrow A$ $(A\rightarrow B)\rightarrow ((B\rightarrow ...
5
votes
2answers
286 views

Who stole the axioms in Natural Deduction?

The study of Gentzen's sequent calculus give me the opportunity to propose some reflections about the concept of logical truth. I'll refer to the english edition of Gentzen's works : The collected ...
12
votes
3answers
382 views

On Pudlak's “Life in an Inconsistent World”

In his Logical Foundation of Mathematics and Computational Complexity (2013), Pavel Pudlak invites the readers to ponder about fictitious people whose natural numbers are nonstandard. His exposition ...
1
vote
1answer
44 views

Enumeration of proofs

Is it possible to enumerate short proofs of short statements, so as to make sure that, say, Goldbach's conjecture doesn't have one of those? How hard would it be? Is it being done? It's seems likely ...
1
vote
1answer
59 views

“Measure” of induction for cut-elimination in sequent calculus

I'm not very familiar with proof thoery, so I'm in trouble understanding different versions of the proof of the Cut-elimination Theorem for sequent calculus. In Sara Negri & Jan von Plato, ...
1
vote
2answers
60 views

Restrictive Rules for LK System

I have a question regarding the restrictive nature of $\forall(R)$ and $\exists(L)$ rules in sequent calculus LK. I don't really understand why the restrictions exists in the first place, so why: $$ ...
3
votes
1answer
53 views

A problem about sequent calculus for classical logic

In Sara Negri & Jan von Plato, Structural Proof Theory (2001), page 51, various properties of the system G3cp of classical propositional logic are showed. Theorem 3.1.1 [page 49] proves that all ...
7
votes
1answer
105 views

Proof-theoretic characterization of the primitive recursive functions?

The total recursive functions are exactly those number-theoretic functions that can be represented by a $\Sigma_1$ formula of first-order arithmetic. Is there a similar characterization of the ...
2
votes
2answers
71 views

Natural Deduction rules for $\lnot$ in classical and intuitionstic logic

Following the very useful answer by Peter Smith to my prevoius post , I'm still reflecting about the "imperfection" connected with the Intro- ans Elim-rules for $\lnot$ in Natural Deduction (I mean ...
1
vote
1answer
36 views

On provability within minimal logic

In its most naive form my question boils down to this: when is a proposition that is provable "by contradiction" also provable "directly"? IOW, is it possible to know, a priori, that a ...
0
votes
3answers
151 views

Using rules of inference (Leibniz) to prove theorems.

Leibniz: If $A \equiv B$ is a theorem, then so is $C[p:= A] \equiv C[p:= B]$. Note: p is "fresh" means p doesn't occur in $A, B, C$. I am trying to understand how to use Leibniz rule of inference for ...
5
votes
4answers
369 views

What is the “correct” reading of $\bot$?

I have some doubts about the "natural" interpretation of $\bot$ in Natural Deduction and sequent calculus. In Prawitz (1965) $\bot$ (falsehood or absurdity) is called a sentential constant [page 14] ...
1
vote
2answers
72 views

A question about consistent fragments of formalized mathematical theories with Natural Deduction

In Dag Prawitz, Natural Deduction A Proof-Theoretical Study (1965), we have the system I of intuitionistic (first-order) logic based on eleven introduction- and elimination-rules : the 3 couples for ...
3
votes
2answers
210 views

How to prove consistency of Natural Deduction systems

In Dag Prawitz, Natural Deduction A Proof-Theoretical Study (1965), we have the system I of intuitionistic (first-order) logic based on eleven introduction- and elimination-rules : the 3 couples for ...
0
votes
1answer
57 views

Prove by Hilbert deduction: ⊢∃x(AvB)→(∃xAv∃xB); ⊢(∃xAv∃xB)→∃x(AvB)

I'd really like your help proving: 1)⊢∃x(AvB)→(∃xAv∃xB) 2)⊢(∃xAv∃xB)→∃x(AvB) Our proof system contains next Hilbert's axioms: 1.A→(B→A) 2.(A→B)→((A→(B→X))→(A→X)) 3.(A&B)→A 4.(A&B)→B ...
3
votes
1answer
112 views

Non-self-referential undecidable sentences in arithmetic

Are there any known undecidable sentences for PA are neither "self-referential" (like a sentence equivalent to its own nonprovability) nor imply consistency of PA (like in the Paris Harrington ...
0
votes
1answer
92 views

Proof by contradiction: May I assume $P$ (true) in $\neg Q \land P \Rightarrow P \land \neg P$ to prove $Q$ by contradiction

Suppose I wish to do a proof by contradiction the statement $Q$. In proving $Q$ may I assume $\neg Q \land P$ (where $P$ is a statement known to be true) and show the implication $\neg Q \land P ...
3
votes
2answers
98 views

Probabilistic “proof” that a sentence is provable (proof “density”).

Is it possible to (or even useful) to calculate the probability that a certain statement is provable? I had this idea that any two statements say A and B could be compared to each other by comparing ...
90
votes
11answers
10k views

Do we know if there exist true mathematical statements that can not be proven?

Given the set of standard axioms (I'm not asking for proof of those), do we know for sure that a proof exists for all unproven theorems? For example, I believe the Goldbach Conjecture is not proven ...
1
vote
0answers
51 views

What is the proof-theoretic strength of the predicative second-order theory of real numbers?

The first-order theory of real numbers, AKA the theory of real closed fields, is obtained by added to the axioms for ordered fields an axiom schema of completeness, which states that for each formula ...