2
$\begingroup$

Lets work with Harvey's Friedman theory ${\sf K}(W)$, formulated in the language of set theory with a primitive constant symbol $W$ added, i.e. in ${\sf FOL}(\in,W)$

Axioms:

Extensionality: $$\forall Z \, (Z \in X \iff Z \in Y) \implies \\\forall Z \, (X \in Z \iff Y \in Z)$$

Subworld Separation: $$\forall A \in W \, \exists X \in W \, \forall Y \, (Y \in X \iff Y \in A \land \phi)$$; where formula $\phi$ doesn't use the symbol "$X$".

Reducibility: if $\phi$ is a formula in ${\sf FOL} (\in)$, with all parameters among "$X,\vec{P}$ " then: $$\forall \vec{P} \in W [ (\exists X: \phi) \implies \exists X \in W: \phi]$$

/

Which is equiconsistent with ZFC.

Is it consistent to add the following principle:

Generalization: if $\phi$ is a formula in ${\sf FOL} (\in)$, with all parameters among symbols "$X,\vec{P}$ "; then: $$ \forall \vec{P} \in W [(\forall \operatorname {infinite} X \in W: \phi) \implies \phi(W)]$$

$\endgroup$

1 Answer 1

2
$\begingroup$

Generalization holds in K(W). Suppose it did not, that ¬𝜙(W) holds and ∀infinite𝑋∈𝑊:𝜙.

Then ∃X((infiniteX)∧¬𝜙), since this is true when X is W. By Reducibility

∃X∈W((infiniteX)∧¬𝜙). But this contradicts the fact that ∀infinite𝑋∈𝑊:𝜙.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.