Questions tagged [formal-proofs]

For questions about proofs within a formal system, such as natural deduction or Hilbert system.

Filter by
Sorted by
Tagged with
0
votes
0answers
60 views

Are any well known conjectures proved to be provable or falsifiable and yet not proved or falsified?

Are there any well known conjectures that are proved to be provable or falsifiable and yet not proved or falsified? Let me give an example. Consider the statement: "There is a natural number $x$ ...
0
votes
0answers
45 views

datebase of formal mathematics

I am learning Logic and set theory, in the process I have made some formal proofs, but this is tedious with the traditional tools. Now, I am wondering if there exists some software or something like a ...
0
votes
1answer
28 views

Showing that $\lim_{x\to c} f(x) > \alpha \Rightarrow f(c+h) > \alpha$ for $|h| < \delta $ where $\delta > 0 $

The question is as follows : Let f : (a,b) $\to \mathbb{R}$ and c $\epsilon$ (a,b) be such that $\lim_{x\to c} f(x) > \alpha$. Prove that there exists some $\delta > 0 $ such that $f(c+h) >\...
2
votes
1answer
72 views

How to justify claims on the complexity of formal proofs without definitions, as described in "Type Theory and Formal Proof" by Nederpelt and Geuvers

In the chapter Definitions of "Type Theory and Formal Proof" by Nederpelt and Geuvers, they start with some motivating examples and then state (with my emphasis added) [T]here is also a ...
0
votes
0answers
39 views

Reverse deduction theorem for predicate logic

I cannot find a name for this metatheorem. By reverse deduction theorem I mean $\Gamma \vdash \phi \to \psi$ implies $\Gamma, \phi \vdash \psi$. There is another question regarding this but for ...
1
vote
0answers
61 views

Q. Is there a formal definition of the word "rigorous"?

I would like to ask if there is a formal definition of the word "rigorous". I think I have a grasp of the concept of "formal stuffs" but I feel like the word "rigorous" ...
2
votes
1answer
241 views

⊢∃𝑥(𝜙⟹∀𝑥𝜙) using Hilbert-style proof [duplicate]

I am tasked to find a proof of $\vdash \exists x (\phi \implies \forall x \phi)$ by using the Hilbert axioms. I've been trying for about 2 hours. I tried using the results from the previous parts of ...
0
votes
1answer
12 views

What is the lower ordinal bound for the smallest fixed point of derivations with infinitary rules

Assume $J$ is a set (of judgments). A rule is a pair $(P,c)$ with $P\subseteq J$ and $c\in J$ with the reading that $P$ is a set of preconditions and $c$ is the conclusion. A system of rules is a set $...
0
votes
1answer
54 views

How do I prove Separation Schema within ZFC?

I am assuming consistency of ZFC throughout this post. Here are what I believe is correct, but please correct me if I am wrong: Every formal proof within ZFC uses finite fragment of ZFC. Separation ...
1
vote
0answers
54 views

Should you avoid using the same variable name after existential elimination?

Existential Elimination (also called Existential Instantiation) says: $$ \exists x[P(x)] \vdash P(c) \text{ For some c} $$ I was wondering whether it's bad form to use the same variable $x$ to ...
0
votes
0answers
32 views

A simpler axiom for "induction" in untyped lambda calculus

I'm working on a weird proof system involving reductions in the lambda calculus. I'm thinking of including the following axiom: ...
3
votes
1answer
59 views

Clarification regarding substitution in sequent calculus

Wikipedia's Sequent Calculus article states: $A[t/x]$ denotes the formula that is obtained by substituting the term $t$ for every free occurrence of the variable $x$ in formula $A$ with the ...
2
votes
1answer
48 views

Natural deduction and introduction of universal quantifier

I have a hard time with quantification introduction and elimination ; for instance, if I want to prove $$\forall x \quad (Px\rightarrow Px ) $$ I am tempted to do the following : $$\underline{[Py]}_{\,...
1
vote
1answer
53 views

How to prove this theorem in this hilbert system

I want to find a proof for $((\alpha \rightarrow (\beta \rightarrow \gamma))\rightarrow ((\alpha \rightarrow \beta)\rightarrow(\alpha \rightarrow \gamma)))$ with these three axioms: Ax1: $(\alpha \...
1
vote
0answers
161 views

Prove $(\alpha \rightarrow \lnot \alpha)\rightarrow \lnot \alpha$ with this hilbert system

I want to find a proof for $(\alpha \rightarrow \lnot \alpha)\rightarrow \lnot \alpha$ with these three axioms: Ax1: $(\alpha \rightarrow(\beta \rightarrow \alpha))$ Ax2: $((\alpha \rightarrow (\beta \...
2
votes
2answers
103 views

How to justify that $\neg A \vee A$ has a sense?

We do substitutions from the set of axioms that we have to prove some statement. I can't understand what actions we should do to go from (1) to (2). What kind of substitution should be made? The ...
0
votes
2answers
60 views

Generalization of nonexpressibility of solutions

Are there any ideas/areas of math that generalize the idea of when a solution to a question can be expressed in some given formal system? Something that (at least in spirit) covers results like No ...
2
votes
0answers
48 views

Help with metalogic induction proof involving string parsing

I have a formal language (basically language of first order logic) in which Wffs are defined by following. String $A$ is a Wff if it satisfies one of: $A$ is atomic $A \equiv (\lnot B)$ and $B$ is a ...
1
vote
1answer
96 views

Using natural deduction to show $(\neg s \to t) \land \neg (s \land t) , k \to \neg f, t \to k \vdash f\to s$

Could someone please tell me if i have proved this sequence correct or not? Is it ok to state e.g. ¬f in row 7, but then assume f in row 13? ...
0
votes
0answers
104 views

Are the Peano Axioms necessary to prove $\forall{x}\exists{y}\ x<y$ (LPL 16.41)

[This is problem 16.41 in Barwise & Etchemendy's "Language, Proof, and Logic".] The only premise given is $\forall{x}\forall{y}\ (x<y \iff \exists z (x+s(z)=y))$ From this, it asks ...
1
vote
1answer
66 views

Fitch - Formally prove that these two premises lead to ∃x(Small(x)) using ∃ Elimination

∃x(¬Large(x)) ∀x(Large(x)∨Small(x)) So far I have this: How do I get to the goal of ∃x(Small(x))? Am I missing something small or am I doing it completely incorrect?
1
vote
1answer
303 views

Proving Infinite Intersection of (-1/n,1/n) To Be The Zero Set

I am looking for a bit of guidance as I am examining some of the methods of proofs of infinite unions and the proper methods to doing so. I am hoping perhaps you will understand my question, I worry ...
0
votes
4answers
51 views

How to disproof with logic: If the digit sum is dividable by 3 the number is dividable by 12 for ℕ ∩ [12, 100)

Assumption: If the digit sum of $x ∈ ℕ ∩ [12, 100)$ is dividable by 3, it is also dividable by 12. Examples: $12 → 1+2 = 3$;$3 \mod 3 = 0 \Rightarrow 12 \mod 12 = 0$ $13 → 1+3 = 4$;$4 \mod 3 = 1 \...
1
vote
2answers
100 views

false introduction sequent calculus?

I'm proving the following proposition using sequent calculus. I got stuck at the very top line. My thought is that if the both hypothesis inside the curly bracket are true, then it's false. So I think ...
2
votes
1answer
65 views

When first encountering a set of primitive inference rules, how do we approach the derivation of the very first derivable inference rules?

I'm currently learning Ebbinghaus et. al.'s propositional calculus in their book Mathematical Logic, and I'm trying to derive the very basic rules of inference such as $\land$ introduction, the law of ...
1
vote
1answer
51 views

Proving Sequent Calculus Statement

I have to prove the sequent $$\vdash (\lnot A \lor \lnot B) \to \lnot (A \land B)$$ using the inference rules for natural deduction listed here (pp. 7-8). I'm super new to natural deduction and ...
0
votes
0answers
36 views

Advanced mathematical proof by induction involving fibonacci numbers [duplicate]

Given the Fibonacci numbers $ F_1 = 1, F_2 = 1, F_n = F_{n-1} + F_{n-2} $. How can I prove $ F^2_{n+1} - F_n F_{n+2} = (-1)^n $ by induction? I have spent hours on this and have arrived no closer to ...
0
votes
1answer
76 views

Proving recursive functions and propositions [closed]

Suppose that I have coded a recursive function foo(i,j,k) and I would like to prove that it returns the correct value for all valid inputs ...
2
votes
2answers
160 views

Notation to indicate that $t$ is substitutable for $x$ in formula $\phi$?

The rules of inference for quantifiers in first order logic involve replacing variables in expressions with other terms. One way to define the substitution $\phi[t/x]$ is that $\phi[t/x]$ arises from $...
2
votes
1answer
53 views

Undo a weakened statement in sequent calculus later in the inferences

I'm working on an answer to (b) of Mathematical Logic, Ebbinghaus et. al. 1984 p. 64 Consider the following inference: $$ \frac{\begin{align}\Gamma \vdash A\\ \Gamma \vdash B\end{align}}{\Gamma \vdash ...
-1
votes
1answer
134 views

What is the exact, formal statement of Gödel's first incompleteness theorem?

I am looking for the explicit formal statement of Gödel's first incompleteness theorem in a formal language (which I assume is the language of first-order Peano arithmetic), permitting only the ...
1
vote
0answers
28 views

Need help proving theorem for limits of multivariable functions (parabola approach)

Suppose I have a function $f:R^2 \to R$, where $R$ are the reals. I want to prove that $$\lim_{(x,y) \to (0,0)} f(x,y) = L \implies \lim_{x \to 0} f(x,mx^2) = L$$ by using a $(\varepsilon, \delta)$ ...
2
votes
0answers
55 views

Prove Power Rule for Limits: $\lim_{x \to a} f(x)^{g(x)} = \left(\lim_{x \to a} f(x)\right)^{\lim_{x\to a} g(x)}$ [duplicate]

Suppose $\lim_{x \to a} f(x) = L$ $\lim_{x \to a} g(x) = M$ I would like to prove $$\lim_{x \to a} f(x)^{g(x)} = \left(\lim_{x \to a} f(x)\right)^{\lim_{x\to a} g(x)}=L^M$$ I thought this had ...
0
votes
1answer
60 views

If a and b are positive integers satisfying $(a^{([2n-1]^2)}) \vert b^{([2n]^2)}$ and $b^{([2n]^2)} \vert (a^{([2n+1]^2)})$ prove a = b.

Recently encountered this question: If a and b are positive integers satisfying $(a^{([2n-1]^2)})\ \vert \ b^{([2n]^2)}$ and $b^{([2n]^2)} \ \vert \ (a^{([2n+1]^2)})$ prove $a = b$. My calculations ...
0
votes
0answers
112 views

Prove that $f'(x) = \lim\limits_{h \rightarrow 0} \dfrac{f(x+h)-f(x-h)}{2h}$ using the definition of a derivative at a point [duplicate]

I know that there is a question that is the same as this, but I wanted to know how to do this using only following definition of a derivative: $f'(x) = \lim\limits_{h \rightarrow 0} \dfrac{f(x)-f(p)}{...
2
votes
0answers
70 views

Simplest set of axioms and inference rules for first-order logic?

I'm interested in finding the "simplest" formulation of first-order logic. To be precise, what formulation of first-order logic has the fewest total axioms (or axiom schemas, henceforth just ...
5
votes
2answers
88 views

strong completeness of a formal system

Given a formal system $D$ where the axioms are the same as in Hilbert system for propositional logic and the inference rule is $$\frac{a\rightarrow b, \quad a\rightarrow \neg b}{\neg a}$$ I need to ...
8
votes
2answers
150 views

How does $\exists !x:P(x)$ allow the definition of a new constant in formal logic?

In everyday math, if we ever prove the existence of a unique object with a certain property, we tend to give it a name and refer to it as "the" such-and-such object moving forward. For ...
1
vote
1answer
120 views

Fitch natural deduction proof of $\exists xF(x) \lor \exists xG(x) \vdash \exists x (F(x) \lor G(x))$

I'm trying to create a natural deduction proof using the openlogicproject proof checker, but I just can't get it right. I have proven this on paper but I don't know how to get this right on the ...
-1
votes
1answer
39 views

Problem with the Formal Definition of a Limit [closed]

Problem: Let $F$ and $G$ be functions such that $0\leq F(x)\leq G(x)$ for all $x$ near $c$, except possibly at $c$. Show that if $\lim_{x\rightarrow c} G(x)=0$, then $\lim_{x\rightarrow c} F(x)=0$. I ...
3
votes
2answers
182 views

Is the wf $B \to \forall x B$ logically valid?

So I wanted to know If $B \to \forall x B$ is logically valid. I found this Tree proof generator website where I can check If a wf is logically valid or if there is an counter-example. I putted in the ...
1
vote
0answers
84 views

How do you formalize this reasoning?

There is this simple number theory problem which says "how many 4 digit numbers that are divisible by 3 and whose digits exclude 2, 4, 6 and 9 exist?" the solution is quite intuitive: each ...
0
votes
0answers
32 views

Equivalence of definitions of maximal consistency

I call a set of formulae $A$ in propositional calculus maximal consistent iff $A$ is consistent and for any formula $\phi$ either $A \vdash \phi$ or $ A \vdash \neg \phi$. I want to prove that this ...
1
vote
1answer
23 views

Can we find grammar for every CFL without $ε $ with these productions

So we have a CFL that doesn't have $ε$ and I have to prove that we can find a grammar for that language with all productions like this $A->BCD$ or $A->a$. I'm thinking about dividing $A->BCD$ ...
2
votes
2answers
37 views

How to prove that my CFG grammar generates $L_1$

I had to come up with a CFG for language $L_1=$$(a+b)$*$-L$ where $L =$ {$a^nb^n: n∈N$} . So my CFG has these $S\to a\mid b\mid bS\mid Sa\mid aSb\mid bSb\mid aSa$ . And I am pretty sure that it ...
0
votes
1answer
40 views

How to prove that L* is context free?

Let's say we have a language of form: $L =$ {$a^nb^n: n∈N$}. I want to prove that $L^*$ is a context-free language. How do I approach this problem? I know that $L$ generates CFG (context-free grammar) ...
0
votes
1answer
32 views

$(\bigcup_{\alpha \in J} (U_\alpha \times V_\alpha)) \cap (A \times B) = \bigcup_{\alpha \in J}((U_\alpha) \cap A) \times (V_\alpha \cap B))$

I'm trying to prove that if $X$ and $Y$ are sets and $A \subset X$ and $B \subset Y$. Then for every element $\alpha \in J$ in an indexing set $J$. If you let $U_\alpha$ be a subset of $X$ and $V_\...
3
votes
1answer
66 views

Is it admissible in a Fitch proof to use $\to$ introduction that "cuts across" subproofs and doesn't discharge them?

There is a certain on-line theorem prover the produces Fitch proofs that occasionally look like this: It uses $\to$ introduction that doesn't seem legit in that it doesn't seem to discharge a whole ...
0
votes
0answers
11 views

What are some common invalid forms in set theory and equational reasoning?

This is a reference recommendation.An argument is valid if it is impossible for the conclusion to be false and premises be true. a sentence form may be obtained from a concrete sentence by replacing ...
1
vote
3answers
97 views

Formal Proof of "No Largest Number"

I need to create a formal proof of there not being the largest number, with only the definition of "less than" being given with Peano arithmetic. $s(x)$ means successor of $x$ or $x + 1$. $$ ...

1
2 3 4 5
15