Re: Implementable Set Theory and Consistency of ZFC

Han de Bruijn <Han.deBruijn@xxxxxxxxxxxxxx> writes:

MoeBlee wrote:

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?

No.

Wow. Are you willfully stupid? You can't be this ignorant by
accident, I think. Moe wrote a clear, coherent proof. You really
claim not to understand it? Which step is unclear?

--
Jesse F. Hughes

"When you try to kiss a girl, it's hard not to get spit on the girl."
-- Quincy P. Hughes, age 3 (almost 4)
.

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
    ... a statement is a valid premise for proving that the integral of 1/t ... 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 ...
    (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 ... 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)