# Questions tagged [formal-proofs]

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

536 questions
Filter by
Sorted by
Tagged with
3answers
824 views

### Prove $( \lnot C \implies \lnot B) \implies (B \implies C)$ without the Deduction Theorem

The issue is Exercise 1.47 (d) in Elliot Mendelson's "Mathematical Logic". The exercise is to prove $(\lnot C\implies\lnot B)\implies(B\implies C)$ by using the three axioms $(A1,A2,A3)$ without using ...
2answers
137 views

### Hilbert's style proof (FO logic)

I am stuck with this question to check whether the following formulas are valid and if they are valid, then derive them using Hilbert's axiom schema and Modes Ponens for First Order Logic. \begin{...
1answer
85 views

### Proofs of Sets and Subsets

I have these proof problems that I need some help on, any direction would be great. Thanks Let A, B, and C be subsets of some universal set U (a) Prove the following: IF $A \cap B$ $\subseteq$ C, ...
1answer
246 views

### Formal Proofs: $\vdash Py \land \exists x Qx \rightarrow \exists x (Py \land Qx)$

First order logic, Hilbert's System. For those familiar with Enderton's Introduction to Mathematical Logic, I am allowed the same axioms. For those unfamiliar, I can use these axioms: ...
1answer
191 views

### Modus ponens proof

I'm trying to prove that $\neg\bullet\varphi$ in system $L(\neg, \to, \bullet)$, $\bullet \varphi \approx (\varphi \to \varphi)$ Axiomas are the followind: A1) $\neg\neg\bullet\bullet\varphi$ A2) ...
1answer
882 views

### Stuck on First-Order Logic

I'm taking a first-order logic class and I keep finding myself stuck on proofs that ask for disjunction elimination and then supply additional premises with conjunctions. How can I eliminate negations ...
1answer
189 views

2answers
55 views

### Prove distribution of or over implies knowing the implication is always true

I was given a task to construct a Hilbert-style proof for the following: $A → B ⊢ C ∨ A → C ∨ B$ I figured I could use the axiom $A→B≡A∨B≡B$, but this leads me nowhere since I don't think I can use ...
1answer
28 views

### Formal proof method for predicate logics

I am looking for the official name for a proof method, The method consists of proving the INconsistency of a theory. This was done using trees. We call it classic-elimination method but I don't know ...
1answer
93 views

### show that for every consistent theory there is a complete consistent theory

Let $\mathcal{L}$ be any language of predicate logic, $\Sigma_0$ a consistent theory in $\mathcal{L}$. Let P be the set of all consistent theories $\Sigma \supseteq \Sigma_0$ in $\mathcal{L}$. With ...
3answers
35 views

### Prove that a sequence which converges at L, still converges at L when a fixed positive integer is added to the variable.

Here is the problem I am attempting to solve/prove: Let $(a_n)$ n∈N be a sequence that converges to L and let p be a fixed positive integer. Prove that the sequence $(a_{n+p})$ n∈N converges to L. I'...
2answers
69 views

### Complement function: how to prove surjective?

Given some set A and a complement function C(K) = A - K from the power set of A onto the power set of A, how can I formally prove that it is surjective? I think I get it, but can't get it on paper. (...
1answer
241 views

### Inductive proof using Fitch software

I am trying to prove the integer square root theorem $\forall x: \mathbb{N}, \exists y : \mathbb{N}((y^2 \leq x) \land (x < (y+1)^2))$ for $\lfloor \sqrt{x} \rfloor$. In words: for any natural ...
1answer
76 views

### Fitch Style Proof

¬(A↔B) conclusion ¬A↔B I'm having trouble with the second part of this proof. I think I managed the first part: 1 |¬(A↔B)$\,$ $\,$ A prem. 2 ||B $\,$ $\,$ A →intro 3 |||A $\,$ $\,$ ...
2answers
148 views

3answers
5k views

### How to prove a logical implication?

Question: Using the Laws of Logic and Rules of Inference, prove that $$(\neg(\neg p \lor q) \lor r) \Rightarrow (\neg p \lor (\neg q \lor r)).$$ I just don't know how to apply the Rules of ...
1answer
72 views

### Context-free language or not

It is language: $L = \left\lbrace a^ib^jc^kd^l \mid i+k < j+l+3 \right\rbrace$ Is it context-free or not? I have two versions: 1)Pumping lemma(refute): get a word $uvxyz = aabcd$ if $i=2$ we get ...
2answers
516 views

### Prove that the following argument is valid

I'm asked to show that the following argument is valid: P1) $[E \lor (L \lor M)] \land (E \leftrightarrow F)$ P2) $L \rightarrow D$ P3) $D \rightarrow \neg L$ C) $E \lor M$ Here is my work (so ...
1answer
77 views

### Iterating proof step

Many books proves theorems by performing one proof step and using this step as a scheme they say by repeating this step $l$ times we prove that... I wonder whether there is some formal meta-theorem ...
3answers
288 views

1answer
173 views

### Formal Proofs: $\vdash \exists x (Py \land Qx) \rightarrow Py \land \exists x Qx$

I wish to show $\vdash \exists x (Py \land Qx) \rightarrow Py \land \exists x Qx$ using the Hilbert System in First-Order Logic with the following axioms: Tautologies \$\forall x \alpha \...
2answers
133 views

### Help with semi-formal logic

How do I write semi-formally 'there are only 2 objects in the universe'? My hypothesis is: ∃x∃y(x≠y) Any ideas?