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-* tag.
-1
votes
0answers
14 views
Simple probability equality proof
For given continuous random variable A,B,C and arbitrary continuous function f, and probability density function p, can you help prove/disprove following equality?
p(A, B, f(A,B)) = p(A, B)
p(A, B, ...
2
votes
1answer
58 views
Can we prove this proposition without thinking semantics?
Let $A$ be a set of propositional symbols, $\alpha$ ba a WFF on $A$ and $M$ be a subset of $A$. And let $M^+: = M \cup \{(\neg a): a\in (A-M)\}$. Then, only one of $M^+ \vdash \alpha$ or $M^+ \vdash ...
0
votes
3answers
56 views
Name of the basic property of equalities that if a=b then f(a)=f(b).
A basic, fundamental property of equalities is that, if one applies a function on both sides of an equality, the equality still holds. Formally: for any two objects $a$ and $b$ of type $T$ and a ...
0
votes
0answers
9 views
Functor to represent directed acyclic graphs for (co)induction
The general theory of induction and coinduction is usually presented in terms of initial algebras and finial coalgebras for certain endofunctors (monads) on the category of sets. (See for example ...
2
votes
0answers
77 views
ZFC plus HOL-Standardness
I was wondering what happens if we extend ZFC by the assumption that $U$ is a model of ZFC that is 'standard' relative to every definable higher-order theory that is categorical. Specifically:
Let ...
0
votes
0answers
35 views
Cut elimination in contextual modal type theory
I'm studying intuitionistic contextual modal logic, presented Contextual Modal Type Theory, by A. Nanevski, F. Pfenning, and B. Pientka (2008). They state the following cut admissibility theorem for ...
2
votes
2answers
45 views
Does the deduction theorem hold in Q?
The proof of the deduction theorem (for a system including Hilbert Calculus) that I am familiar with uses modus ponens to prove the result one way, and mathematical induction the other way.
Robinson'...
5
votes
3answers
372 views
How can we prove that any integral in the set of non-elementary integrals cannot be expressed in the form of elementary functions?
We know that the derivative of some non-elementary functions can be expressed in elementary functions. For example $ \frac{d}{dx} Si(x)= \frac{\sin(x)}{x} $
So similarly are there any non-elementary ...
1
vote
0answers
17 views
Does the order of applying rules in Sequent Calculus matter?
Suppose we want to prove some $\Gamma \models \Delta$ in (first-order logic) sequent calculus LK.
We start with the sequent $\Gamma \vdash \Delta$, and arbitrarily apply rules backward until we reach ...
2
votes
1answer
60 views
How to deduce $\square p\to p$ from other modal axioms?
I'm trying to deduce the T axiom $\square p\to p$ from the B,D,5 (and also K) axioms.
B: $q\to\square\diamond q$
D: $\square q\to\diamond q$
5: $\diamond q\to \square \diamond q$
I tried to assume ...
0
votes
0answers
35 views
Is there an ordering of logical systems defined by reductions?
I am aware of the lambda cube which gives an ordering to several variants of the lambda calculus. My intuition says that this ordering should have the following property:
For logics $A,B\in\lambda\...
1
vote
2answers
85 views
Model Theoretical Interpretation of the Incompleteness of Number Theory
This question was sparked by this Numberphile video: https://www.youtube.com/watch?v=O4ndIDcDSGc. Near the end, (12:05), he speaks about the Riemann Hypothesis. He describes that if Riemann is shown ...
0
votes
1answer
36 views
$\vdash\neg(\square \neg p\land p\land\diamond(p\land\square p\land \diamond p) )$
How to show that $\vdash\neg(\square \neg p\land p\land\diamond(p\land\square p\land \diamond p) )$ in the logic K?
First of all, does this proof work? Assume the converse (i.e. that $\vdash\square \...
1
vote
1answer
47 views
Are proofs by “maximality” equivalent to proofs by induction?
I apologize for the lack of proper terminology; I have zero experience in this field.
What I mean by "proof by maximality": One way to show that a set $A$ has a certain property $p$ is to assume ...
0
votes
0answers
42 views
classical logic - rules for quantifiers
I have these formulas of CL:
(a) ∀xP(x,x)
(b) ∀x∀y∀z(P(x,y)∧P(y,z) → P(x,z))
(c) ∀x∀y(P(x,y) → ¬P(y,x)
and I have been trying to prove weather (a),(b) ⊨ (c). First I would use ∀l and then my ...
0
votes
1answer
50 views
Proving that a sentence is inconsistent [duplicate]
I'm trying to understand if the sentence $\square\bot\land \phi$ is consistent in KD. I don't think it is true because it looks like no serial model where this sentence is satisfiable exists. As I ...
2
votes
1answer
58 views
Showing $\vdash \phi\to \square \diamond \phi$
I'm trying to prove the converse of what was shown here.
Namely, I'm trying to prove B-axioms of modal logic ($\vdash \phi\to \square \diamond \phi$ or $\vdash\diamond\square\phi\to\phi$, whatever is ...
1
vote
1answer
44 views
Prove $\vdash \neg(\square F\land p)$ in $KD$
How to prove that $\vdash \neg(\square F\land p)$ in $KD$? The allowed rules are natural deduction rules and the axiom $\square p\to\diamond p$ where $\diamond p=\neg\square\neg p$.
I actually don't ...
0
votes
0answers
15 views
Is it possible to prove that propositional calculus is consistent using only its syntax?
Let us consider Gentzen's propositional calculus with only one axiom:
$$
\phi \vdash \phi
$$
and 12 rules of inference.
As far as I know this PC is consistent, i.e. not all of their expressions (...
-1
votes
2answers
50 views
How is the order of statements gives a different answer? [closed]
arent both statements equivalent? so both should be false?
0
votes
2answers
38 views
Sum of functions is big Oh
I want to show that if
$$
d(n) \in O(f(n)) \ \Rightarrow d(n) \le c_1*f(n) \\ e(n) \in O(g(n))\Rightarrow e(n) \le c_2 *g(n) \\
$$
then
$$
d(n) +e(n) \in O(f(n)+g(n))
$$
Can I say that (A)
$$
d(n) +...
1
vote
1answer
93 views
What is the most expressive logic?
What is the most expressive logic studied in the literature (in terms of expressing properties about a structure in the sense of model theory)?
Many people talk about second-order logic, but third-...
2
votes
1answer
84 views
Formalizing the deduction theorem in the metatheory
Here is the deduction theorem, in the "$\Leftrightarrow$" version (I'm considering it for first order logic):
$$\Delta \cup \lbrace A \rbrace \vdash \lbrace B \rbrace \Longleftrightarrow \Delta \vdash ...
0
votes
1answer
19 views
Prove that real-values function $f$ on the interval $(x_0 - r , x_0 + r)$, is analytic at $x_0$
Let F be a holomorphic function defined in an open disk $D(x_0, r)$ where $x_0 ∈ R$.
Define a function $f$ in the interval $(x_0 − r, x_0 + r)$ by $f(x) = F(x$) for all
$x ∈ (x-0 − r, x_0 + r)$. ...
2
votes
2answers
51 views
Do type constructors have type themselves?
I'm recently trying to understand the basics of intuitionistic type theory, and I think I have grasped much of it. However, there is this question on my mind. For instance, can the type constructor $\...
2
votes
1answer
29 views
Can $\kappa$-club is defined for any class of ordinals?
In reading "Proof Theory - The First Step into Impredicativity", I'm stuck at Thm. 3.2.19.
3.2.19 Theorem Let $\kappa$ be a regular ordinal. A class $M\subseteq On$ is $\kappa$-club iff $en_M$ is a ...
4
votes
1answer
79 views
How do we know PA is incomparable with PRA + $\epsilon_0$?
Gödel 2 says that no subtheory of PA can prove Con$_{PA}$, and even though most natural theories $T$ extending PA can prove Con$_{PA}$, this is relatively uninteresting since anyone doubting the ...
3
votes
0answers
35 views
Why can't the sequent calculus for First-Order Classical Logic be used for proving decidability via Proof-search?
I understand that Turing reduced the halting problem to the satisfiability problem of first-order logic thus proving first-order logic undecidable. However, when thinking about the sequent calculus ...
4
votes
0answers
257 views
Metamathematics and the foundations of mathematics
I have some really big doubts about what is the real starting point of all (formal) mathematics.
For example: when I search on internet or study texts about the foundations of mathematics such as ...
2
votes
1answer
69 views
Calculation of cut height/depth of a cut in Sequent Calculus
I am having trouble understanding the calculation of an idea, which is called 'cut height' in Negri and von Plato's Structural Proof Theory (SPT), and 'depth of a cut' in Troelstra and Schwichtenberg'...
0
votes
2answers
39 views
Why do we need the commutative axiom of multiplication?
I think I can prove that $ab = ba$ by other axioms. Am I wrong? Why?
Edit: proof updated with notes showing where I actually used the commutative property without noticing.
Proof. For any numbers ...
3
votes
1answer
74 views
Is there a computable and complete “probabilistic” theory of arithmetic?
Let $\mathbb T$ be a probability distribution over complete and consistent theories of first order arithmetic that contain $PA$. Additionally, we will require that for any sentence $\phi$ in the ...
4
votes
3answers
117 views
Why does Gödel's Second Incompleteness Theorem undermine Hilbert's program?
Recall that Gödel's First Incompleteness Theorem (denote GIT1) states, roughly, any axiomatic system $S$ stronger than Peano Arithmetic (PA) cannot be "covered" by finitely many axioms.
GIT2 states, ...
6
votes
2answers
81 views
Can a mathematical proof always be objectively determined as correct or incorrect?
Fields medalist Michael Atiyah claimed a simple proof of the Riemann hypothesis, but many mathematicians rejected his proof. Am I right in saying that Atiyah's proof is either objectively correct (...
1
vote
1answer
83 views
Inversion lemma proof
I am following Structural Proof Theory by Negri and others, and I don't understand the Inversion Lemma proof (i) (the system is G3$_{ip}$, which is the same as G3$_i$ only that it excludes quantifier ...
3
votes
0answers
52 views
What will be the notion of a “valid deduction” in the following system?
Consider the Propositional Calculus whose axiom schemes and rule of inference are given below (here $P,Q$ and $S$ are formula schemes,
$\color{crimson}{\text{Axiom 1.}}\ P\to (Q\to P)$
$\...
3
votes
1answer
81 views
First orderer logic completeness and independence: the proof that disappear?
Gödel completeness theorem for the first-order logic is in fact equivalent to BPI (every proper filter can be extended to an ultrafilter). Moreover, BPI is independent of ZF; that in particular means ...
1
vote
1answer
51 views
Unprovable sentence, but provably it is provable.
Work in Peano Arithmetic, PA. Let Prov(n) be a standard proof predicate, so that $PA \vdash Prov(\ulcorner \phi \urcorner) \text{ iff } PA \vdash \phi$ .
By Löb's theorem, we know that if $PA \vdash ...
18
votes
2answers
916 views
Has a conjecture ever originally been decided by constructing the proof with mathematical logic?
So, one of the things that mathematical logic does is study theorems as abstract objects. There also many theorems about mathematical logic, and these theorems can have connections to other fields.
...
-3
votes
2answers
27 views
Rational Numbers Proof
Apologies for the vagueness before, I'm new here. I hope this clears it up:
Show that, for all non zero $b\in \Bbb Z$, $${(0,b)}=((a',b')\in F:a'=0)$$ $$F=((a,b)\in \Bbb Z*\Bbb Z: b\ne 0))$$ where F ...
3
votes
2answers
32 views
Formal proof of distributivity of conjuction
I'm trying to prove that $\vdash p\land (q\lor r)\to(p\land q)\lor (p\land r)$ in natural deduction.
...
2
votes
1answer
45 views
Provide sequent calculus proofs of the axioms of the $\{→,∀,⊥\}$-fragment of the Hilbert system $H_c$
Could anyone please help me to understand what the question is asking?
Theorem: G1$_i$ + Cut $\vdash \Gamma \Rightarrow A$ iff H$_i$ $\vdash \Gamma \Rightarrow A$
1) Prove equivalence of G1$...
5
votes
0answers
53 views
Axiomatizing a “bounded” companion to PA
There's nothing special about PA here, I'm just focusing on it since it's strong enough to ignore lots of minor technical issues around foundations. If switching to some other theory would yield a ...
0
votes
1answer
33 views
Example of a $Δ_1$-formula that is not $Δ_0$ (arithmetical hierarchy).
In the arithmetical hierarchy, the class of $Δ_1$-formulas is defined as the intersection of $Σ_1$- and $Π_1$-formulas. It is obvious that every $Δ_0$-formula is $Δ_1$, but not every $Σ_1$- or every $...
1
vote
1answer
61 views
If Γ ⊢ A, then Γ ⊨ A
I'm having a difficult time differentiating between the two proofs:
1. If Γ ⊢ A, then Γ ⊨ A
vs.
2. If ⊢ A, then ⊨ A
Here's the question:
Prove “strong soundness”: for any set of formulas, Γ, and ...
0
votes
0answers
81 views
Can you recommend literature - easy/gentle/for self-study/introductory… - for the following topics…?
I am looking for literature that is as self-explanatory, easy, gentle, readable to the beginner, suitable for self-study, etc.. as possible, in the following fields.
(I mean the mathematical part as ...
1
vote
1answer
31 views
Regarding L$\to$ rule in sequent calculus and difference between G1$_c$ and G1$_i$ system
I am going through Troelstra and Schwictenberg's Basic Proof Theory, and I can understand most of the sequent calculus rules by finding some sort of parallel between the rule and a corresponding ...
0
votes
1answer
62 views
Swapping elements to form a specific permutation - Formal Proof
Considering a permutation of [1, 2, ..., n], it is fairly obvious that on doing n/2 swaps we arrive at the permutation [n, n-1, ..., 1].
This can be achieved by swapping the first element with the ...
2
votes
4answers
100 views
Proof of $(P\to Q) \vee (Q\to P)$ with natural deduction
I need to prove the following statement in natural deduction:
$$(P\rightarrow Q) \lor (Q\rightarrow P)$$
I tried assuming not (target statement) and assuming the left hand side, but I don't know ...
1
vote
4answers
74 views
Formal Deduction (logic) Question: $\lnot C, (B \to \lnot C) \to A \vdash (A \to C) \to F$
I've been stuck on this question for around two hours now.
I'm trying to prove that:
$\lnot C, \ (B \to \lnot C)\to A \vdash (A \to C)\to F $
I'm trying to get my second last step to be:
$\lnot C,...
