Re: Contradiction or paradox

On May 19, 3:42 pm, Charlie-Boo <shymath...@xxxxxxxxx> wrote:
On May 19, 4:24 pm, "Jesse F. Hughes" <j...@xxxxxxxxxxxxx> wrote:

Charlie-Boo <shymath...@xxxxxxxxx> writes:
See, I repeat, you have not shown that subtraction satisfies the
hypotheses.

What hypotheses? You have given no hypotheses.

You pathetic liar.

self-applied

That's jejune. Over half a dozen people have pointed out the
hypotheses to you.

Right here is the theorem we have been discussing:
http://us.metamath.org/mpegif/ecoprass.html

Here is the top of that page. Apologies for typographic oddities
resulting from cut-n-paste.

Description: Lemma used to transfer an associative law via an
equivalence relation.

Hypotheses
------------
ecoprass.1|- D = ((S X. S)/.R)

ecoprass.2|- (((x e. S /\ y e. S) /\ (z e. S /\ w e. S)) ->
([<.x, y>.]RF[<.z, w>.]R) = [<.G, H>.]R)
ecoprass.3|- (((z e. S /\ w e. S) /\ (v e. S /\ u e. S)) ->
([<.z, w>.]RF[<.v, u>.]R) = [<.N, Q>.]R)
ecoprass.4|- (((G e. S /\ H e. S) /\ (v e. S /\ u e. S)) ->
([<.G, H>.]RF[<.v, u>.]R) = [<.J, K>.]R)
ecoprass.5|- (((x e. S /\ y e. S) /\ (N e. S /\ Q e. S)) ->
([<.x, y>.]RF[<.N, Q>.]R) = [<.L, M>.]R)
ecoprass.6|- (((x e. S /\ y e. S) /\ (z e. S /\ w e. S)) ->
(G e. S /\ H e. S))
ecoprass.7|- (((z e. S /\ w e. S) /\ (v e. S /\ u e. S)) ->
(N e. S /\ Q e. S))
ecoprass.8|- J = L
ecoprass.9|- K = M

Assertion
-----------

ecoprass|- ((A e. D /\ B e. D /\ C e. D) -> ((AFB)FC) = (AF(BFC)))

The formulas ecoprass.1-9 are clearly listed as hypotheses which must
be verified before the conclusion is justified. And this is exactly
how the theorem is later applied to addition:

Thanks.

Thanks for what? Yeah, thanks for Jesse copying/pasting what YOU were
supposed to read originally and could have read over the course of
about two years while you've claimed that Megill's system is
inconsistent.

How is that later justified, as you say?

Look at the proof! Each line in any proof in Megill's presentation IS
LITERALLY machine checked (as opposed to what we ordinarily claim to
be machine checkable if only in principle). So read each proof line by
line, and with its LINE BY LINE ANNOTATION if you want to know the
justification of any line whatsoever in any of his proofs. Sheesh!

What I posted ages
ago did not show any checks when the substitution is made.

Whatever the dickens that is supposed to mean, what you posted did not
show that subtraction satisfies the hypotheses, and that is what is at
issue here.

I see statements about all of mathematics coming from a small number
of axioms - ZF, some logic, Peano's Axioms - but in the proofs I see
hundreds of axioms, rules, definitions. I also wonder why simple
proofs take hundreds of lines. Can't we prove 2+2=4 in a few steps (2
is 0'' and 4 is 0'''' etc.)?

There are not hundreds of axioms and rules. As to definitions, they
are ways of abbreviating, so of course in a system such as Megill's
which is syntactically precise, there will be lots and lots of
abbreviations of things that have been worked out along the way in the
system. We can have lots and lots of definitions and still have all
our results derivable from the axioms, since we can eliminate any
defined term and write it in primitive notation. That you even raise
this as an issue indicates once again that you are confused and
ignorant regarding some of the very basic concepts of axiomatic
systems.

As to the number of lines it takes to proof things, that is a result
of the very rigor of the system. The fewer axioms and primitives
combined with the demand in Megill's system that there are no informal
summaries allowed in place of purely machine checkable syntax results
in a lot of lines of proof.

1. Where did the lines in the proofs come from - what creates them?

One figures out ways to prove things, then writes them in the formal
language. And then, in Megill's system, those lines in the formal
language are machine checked to verify that each line is an axiom or
definition or follows from previous lines by a rule.

Why are you asking these questions? Haven't you READ the material that
addresses this on his web site?

2. What assures that they follow some specific syntax? What if they
don't follow the correct syntax?

If I'm not mistaken, you can even download the program code that does
the syntax checking. (?)

3. Can the general public use the system to create proofs
automatically? If yes, then how, and if no, then why not?

What do you mean by "the general public"? Anyway, Megill gives
explanations for how to work in the system and to create proofs. I
don't see anything about his system that would not be comprehensible
to someone with a modest familiarity with mathematical logic and
mathematical proof. Also, there are two separate matters: On the one
hand, is automatically creating proofs, which should by answered by
yourself in view of the fact that the theorems are recursively
enumerable, and on the other hand, is machine checking that a sequence
of formulas is indeed a proof.

4. What is creating the massively long expressions that occur? How do
we know that they are correct? How do we know that they are
meaningful?

You can check them yourself in using yourself as the subject of the
'competent clerk' notion of computability. Oh wait, nevermind, you've
already proven yourself incompetent by your cursor moving right past
the lines that are the hypotheses of the theorem we've been
discussing.

As to meaning, you should be familiar with the ordinary notions of
semantics for such formal languages.

5. When did he most recently add a new axiom, rule, definition etc. to
the system?

I don't know the timeline of his project.

What is the source of the complete sets of axioms, rules,
definitions etc.?

Complete in what sense? We prove a completeness theorem for first
order logic, and it don't think there would be much difficulty in
showing that his system is complete in that sense.

Do you have to keep adding to the system to prove
all statements of arithmetic such as 2+(3*5)=17?

What do you mean by "adding"? Do you mean adding an axiom? No, I don't
think you have to add axioms to prove such equalities as you
mentioned.

And if my answers suggest any more questions for you, I suggest you
read more at his own site, since I am not his FAQ, and since you have
already demonstrated a willingness to fire off a bunch of questions
based on your own unwillingness to simply read what is at the site
first.

First, check that
addition satisfies the hypotheses and then conclude that it satisfies
the conclusion.

You have never shown that subtraction satisfies these nine hypotheses.

Ah, again, this is the point Charlie-Boo keeps missing.

MoeBlee

.