Re: Implementable Set Theory and Consistency of ZFC

On Oct 31, 4:13 am, Han de Bruijn <Han.deBru...@xxxxxxxxxxxxxx> wrote:

So, even if I don't make use of (5-8), a proof of A from (1-4) is a
proof from (1-8) ? So, even if I say "there exists a Foo", then such
a statement is a valid premise for proving that the integral of 1/t
from 1 to x is ln(x) ? Weird ..

No one said anything about "valid premise".

Here is the definition (I'm giving it a bit informally, it be can be
made even more precise, but this is good enough for our purposes),
and, for convenience, I'll use Hilbert style proof (it's easy to adapt
this to other systems such as natural deduction):

P is a proof of S from G iff
P is a sequence of formulas in the language such that every entry in
the sequence is either an axiom of logic (with identity if identity
theory is used or needed) or a member of G or follows from previous
entries in the sequence by an inference rule, and the last entry in
the sequence is S.

Then

Theorem: If P is a proof of S from G, and G is a subset of H, then P
is a proof S from H.

Proof:
Suppose P is a proof of S from G, and G is a subset of H.
Then P is a sequence of formulas in the language such that every entry
in the sequence is either an axiom of logic (with identity if identity
theory is used or needed) or a member of H (SINCE EVERY MEMBER OF G IS
A MEMBER OF H) or follows from previous entries in the sequence by an
inference rule, and the last entry in the sequence is S.

Do you get it now?

MoeBlee








.

Relevant Pages

  • Re: Implementable Set Theory and Consistency of ZFC
    ... P is a sequence of formulas in the language such that every entry in ... the sequence is either an axiom of logic (with identity if identity ... theory is used or needed) or a member of H (SINCE EVERY MEMBER OF G IS ... inference rule, and the last entry in the sequence is S. ...
    (sci.math)
  • Re: Implementable Set Theory and Consistency of ZFC
    ... P is a sequence of formulas in the language such that every entry in ... the sequence is either an axiom of logic (with identity if identity ... in the sequence is either an axiom of logic (with identity if identity ... theory is used or needed) or a member of H (SINCE EVERY MEMBER OF G IS ...
    (sci.math)
  • Re: jmdict: question about ent_seq
    ... can I I use ent_seq to find the exact same entry even after ... First there are 'TempSUB' entries that users ... in the standard jmdict but they have temporary numbers that get changed ... and don't have sequence numbers. ...
    (sci.lang.japan)
  • Re: Implementable Set Theory and Consistency of ZFC
    ... P is a sequence of formulas in the language such that every entry in ... the sequence is either an axiom of logic (with identity if identity ... theory is used or needed) or a member of H (SINCE EVERY MEMBER OF G IS ... inference rule, and the last entry in the sequence is S. ...
    (sci.math)
  • Re: Q:The Mersenne Primes and the Collatz conjecture (3x+1)/2.
    ... > Stating with this is a point of entry into this ... not every MP enters that sequence. ... 341 IS a sub-branch of the powers of 2 ... least two Mersenne Primes pass. ...
    (sci.math)