Re: Scott and George's Teaching Thread


On Aug 23, 12:58 pm, Scott <ToaTe...@xxxxxxxxx> wrote:
So to practise, the subset symbol, denoted as a sideways "u" is also a
macro:
B subset C
means, when B and C are sets
Ax[ xeB -> xeC].

On Aug 23, 5:16 pm, MoeBlee <jazzm...@xxxxxxxxxxx> wrote:
Right,

Right, he IS right, so I will THANK you NOT to CORRUPT
said rightness with further contamination.
I am not as mad today as I was two days ago, though, because the more
complicated it gets, the more likely it is that everybody else's
explanations
will be better than mine.

'subset of' (which is an English rendering of the subset
symbol) is a DEFINED 2-place predicate symbol of the language.

NO, it ISN'T.
I am counting on Scott's programming-language-implementation
perspective
to help HIM keep the DIFFERENCE between a MACRO and things that ARE
IN the language STRAIGHT.

THE ONLY predicate in this language is e. This is IMPORTANT.
LEARNING how MUCH you can do with only ONE predicate is IMPORTANT.
Definitions are important to but the important definitions will be
recursive
(the axiom of foundation is usually present). What is going on with
subset
(and the further definition of = in terms of subset) IS GOING ON IN
A PURE
programming-language-definability sense AND NOT in the theory. INside
the theory, NOBODY CARES how hard anything is to read, or how long it
is!
INSIDE the theory, we can write s(s(s(s(s(s(s(0))))))) ! We DON'T
have to write '7'
BECAUSE IT DOESN'T MAKE ANY [theoretical] DIFFERENCE!
We do, however, have to prefer 7 if we are going to be able to read
what we write.

The
definition:

Axy(x subset of y <-> Az(zex -> zey)).

We add that formula to the axioms of our set theory,

No, we don't. Definitions ARE NOT axioms, although some axioms
should be thought of as definitions. It ABSOLUTELY WILL HELP
your understanding HERE, at the BEGINNING, to treat Def/Thm/Ax as
a trichotomy. "Is this a Def, a Thm, or an Ax?" is a question that
will
SPARE you confusion! ASK IT FREQUENTLY!
Subset as presented here is a Def AND NOT an Ax.

as that formula then is a definitional axiom.

I repeat, don't confuse definitions with axioms, at least not until
you get to axioms whose purpose is to define things.
Specifically, those would be the Axiom of Union and the Axiom of
Power.
Subset is just an abbreviation. It's just syntactic contact lenses,
to ease
your reading. It's not actually THERE.
But if I were going to use macros, I should've defined the subset
macro
first and then defined the = macro in terms of it, yes.

In any case, macro-definition is something that anybody can use
anywhere,
over any language, if they feel up to it. There is nothing about it
that is specific
to first-order languages or first-order logic or set-theory. Which is
why MB
was wrong to be talking about adding "definitional axioms".
I will get around to presenting the axioms presently.
The definition of subset is NOT one of them.
But it was helpful in that it will make the powerset axiom easier to
understand.



.

Relevant Pages

  • Re: Scott and Georges Teaching Thread
    ... Please think of this as a programming language. ... predicate in this language is e. ... The axioms jointly CLARIFY AND EXPLAIN ... Some of these logical primitives are from 0th-order logic; ...
    (sci.logic)
  • Re: Small set Theory:final version.
    ... "P_defined" in the axioms to ... object language but only in meta language. ... predicate is - that there are at most countably many zuhair sets). ...
    (sci.math)
  • Re: Small set Theory:final version.
    ... Hi hagman, I already modefied a lot of the theory that all of this ... "P_defined" in the axioms to ... object language but only in meta language. ... predicate is - that there are at most countably many zuhair sets). ...
    (sci.math)
  • Re: Scott and Georges Teaching Thread
    ... The realm we are about to investigate, set theory, ... ONLY HAS ONE predicate. ... The definition of a first-order language gives rules for combining the ... The purpose of this enterprise is to prove theorems from axioms. ...
    (sci.logic)
  • Re: primitive recursive: obsolete?
    ... we have to add more axioms. ... all true sentences of arithmetic in the language of PA. ... logic we define the set of sentences true in the standard model of PA ... theorems" or not has no bearing on the fact that what I said is ...
    (sci.logic)