2
votes
Accepted
Expressibility of statement in generic extension
Yes, this is doable, but not obvious at all! The definability of the ground model was proved independently by Laver and Woodin. Their proofs relied on the ground model satisfying full $\mathsf{ZFC}$, ...
2
votes
Accepted
Using Fitch System in Coursera
You correctly assume $\exists x p(x)$ and you have to derive a contradiction.
With this assumption, you derive $\forall x q(x)$ by $(\to \text E)$.
From the assumption ,you have to use $(\exists \text ...
1
vote
Accepted
Use induction to prove that it can be determined whether or not the disjunction $A_1\lor\cdots\lor A_n$ is a tautology.
Comments:
page 17: $(A \to B)$ is the abbreviation of $(\lnot A \lor B)$. Thus, $A_1 \to \ldots \to A_n \to B$ amounts to: $\lnot A_1 \lor \ldots \lor \lnot A_n \lor B$.
yes. Removing abbreviations, ...
1
vote
When is a consistent (formal) system sound as well?
Long list of comments
Several issues here: (i) your "system $\mathsf C$" has only one non-logical axiom: $∃x∀y (y \notin x)$. Having the symbol $\in$, this means that we are working in a ...
1
vote
Accepted
First order logic show the following $\neg \exists x(x\neq m )\vdash\forall x \forall y (Px \rightarrow Py)$
Your proof idea is good! Just a few technical details to be fixed:
When you do existential elimination, you need to pick a new constant: a constant that you are not already using in the proof. So, as ...
1
vote
First order logic show the following $\neg \exists x(x\neq m )\vdash\forall x \forall y (Px \rightarrow Py)$
The symbol $m$ is an individual constant and the premise says that there is only one element ("everything is equal to $m$").
Thus, intuitively, it follows that "if something is P, then ...
1
vote
Accepted
How to prove Replacement from Reflection?
You can show in this system that there are many transitive sets which preserve the truth of $\Sigma_n$ formulas for each concrete n, which should be enough to complete a proof of replacement.
Inf: the ...
Only top scored, non community-wiki answers of a minimum length are eligible
Related Tags
first-order-logic × 12642logic × 6950
quantifiers × 1226
model-theory × 1184
discrete-mathematics × 790
propositional-calculus × 771
logic-translation × 449
set-theory × 391
natural-deduction × 347
solution-verification × 343
elementary-set-theory × 320
proof-writing × 227
formal-proofs × 222
peano-axioms × 170
proof-theory × 151
incompleteness × 133
axioms × 132
proof-explanation × 127
notation × 125
definition × 108
foundations × 92
reference-request × 85
satisfiability × 84
formal-languages × 83
induction × 75