Curry's Paradox in propositional logic?

[Dan Christensen]

Can Curry's Paradox be stated in propositional logic as follows:

[A <=> [A => B]] => B

This is a tautology.

Note that:

[A <=> [A => B]] = A & B


Dan

Download my DC Proof 2.0 freeware at http://www.dcproof.com
Visit my Math Blog at http://www.dcproof.wordpress.com

[burs...@gmail.com]

You need less than classical logic, to deduce Curry's
paradox. Thats why it is a paradox.

You can prove it for example in Dragalins G3i. The
proof is non-trivial, it needs quite a depth.

See also here:
https://plus.google.com/+JekejekeCh/posts/WJtCFfd7bNt

But the source code is missing because the server
is gone. I guess I should dig it out, if I have

time. Or just redo the proof and put on gist.

[burs...@gmail.com]

The paradox is related to paraconsistency,
it shows that some non-classical logics can

still react with nonsense to inconsistencies.

[Dan Christensen]

On Friday, June 29, 2018 at 3:31:59 PM UTC-4, burs...@gmail.com wrote:
> You need less than classical logic, to deduce Curry's
> paradox. Thats why it is a paradox.
>

So, it's only a "paradox" is some other form of logic. Whew!

[burs...@gmail.com]

Yes Haskel Brooks Curry was dealing with non-classical
logics. He called it the "absolute system".

See also:
Haskell B. Curry, Foundations of Mathematical Logic
(NY, McGraw Hill, 1963, reprinted by Dover, 1977, 1984).
A Review by Jonathan P. Seldin
https://projecteuclid.org/download/pdf_1/euclid.rml/1204834542

He identified a couple of non-classical logics:


LM: Absolute refutability (Minimal logic), formed by adding introduction rules on both sides for negation to LA.
LJ: Absolute absurdity (Intuitionistic logic), formed from LM by adding ex falso quodlibet .
LD: Decidable refutability, formed from LM by adding excluded middle.
LE: Classical refutability, formed from LC the way LM is formed from LA.
LK: Classical absurdity, formed from LE by adding ex falso quodlibet Decidability holds for this system, which is the classical proposi- tional calculus.

[burs...@gmail.com]

Note that unlike the liar paradox or
Russell's paradox, Curry's paradox
does not depend on what model of
negation is used, as it is completely
negation-free. Thus paraconsistent
logics can still be vulnerable to this
paradox, even if they are immune to
the liar paradox.
https://en.wikipedia.org/wiki/Curry's_paradox#Resolution

[Peter Percival]

Dan Christensen wrote:
> Can Curry's Paradox be stated in propositional logic as follows:
>
> [A <=> [A => B]] => B
>
> This is a tautology.

No. See https://en.wikipedia.org/wiki/Curry's_paradox#Sentential_logic.

[burs...@gmail.com]

Truth table generator tells me its a tautology:

p q ((p ↔ (p → q)) → q)
F F T
F T T
T F T
T T T
http://web.stanford.edu/class/cs103/tools/truth-table-tool/

But its also provable in weaker systems than classical logic.

[burs...@gmail.com]

This variant is also fun:

p q ((p ↔ (p → q)) → p)

F F T
F T T
T F T
T T T

Just define p self referential negatively,
then you can prove it.

[burs...@gmail.com]

I am not sure whether the other variant
can also be proved with weaker than
classical logics.

[Peter Percival]

burs...@gmail.com wrote:
> Truth table generator tells me its a tautology:
>
> p q ((p ↔ (p → q)) → q)
> F F T
> F T T
> T F T
> T T T
> http://web.stanford.edu/class/cs103/tools/truth-table-tool/

My "no" wasn't a reply to Dan's "This is a tautology." but rather to his
question "Can Curry's Paradox be stated in propositional logic as
follows: [A <=> [A => B]] => B". So my "no" was probably in the wrong
place. My apologies if I confused anyone.

[burs...@gmail.com]

This one doesn't work:

p q r ((p ↔ (p → q)) → r)
F F F T
F F T T
F T F T
F T T T
T F F T
T F T T
T T F F
T T T T

Because q and r are not anymore connected,
there is one case where the sentences
is not satisfied.

Then we could also try:

p r (((p ↔ (p → ⊥)) ∧ (p ↔ (p → ⊤))) → r)

F F T
F T T
T F T
T T T

The above simulates a primitive forall q around
the defintion, and we have indeed again a tautology.
Even the worst of all, now r can be really anything.

And we could also try:

p r ((p ↔ ((p → ⊥) ∧ (p → ⊤))) → r)

F F T
F T T
T F T
T T T

Which simulates a primitive forall q of the
definition body, again a very bad situation.
But I think what Dan has posted is usually
considered the propositional form of the paradox.

[Dan Christensen]

On Friday, June 29, 2018 at 3:59:28 PM UTC-4, burs...@gmail.com wrote:
> Thus paraconsistent
> logics can still be vulnerable to this
> paradox, even if they are immune to
> the liar paradox.

A case of the cure being worse than the supposed "disease?"


Dan

[burs...@gmail.com]

Lets say Lx is one of the logics, LM, LE, etc..
that Curry considered. And lets say LK is the
classical logic.

Among the Lx are also some paraconsistent one,
without ex-falso-quodlibet, etc.. Hence being
sub intuitionistic.

But the way Curry has set up everything, its
easy to see, that:

Lx |- A => LK |- A

So what is valid in some of the weaker, maybe
also paraconsistent logics,

is also valid in classical logic. Quiz, so
why would one study a family of

systems Lx? Why is there the area of non-classical
logics in mathematical logic?

[Ross A. Finlayson]

In a (or rather, the) Comenius language,
only truisms are well-formed, so,
no falsity of material implication,
(that being Curry's poor substitute),
no propagation of the liar paradox,
and paraconsistency exists.

[Ross A. Finlayson]

Because the lie is terminal, not generative,
belief in a model is a different story.

[Ross A. Finlayson]

https://en.wikipedia.org/wiki/Curry%27s_paradox#Consequences_for_some_formal_logic

This section quite well reflects the "inductive impasse" discussed.

"In the study of illative (deductive) combinatory logic, Curry in 1941[5] recognized the implication of the paradox as implying that, without restrictions, the following properties of a combinatory logic are incompatible:

Combinatorial completeness. This means that an abstraction operator is definable (or primitive) in the system, which is a requirement on the expressive power of the system.
Deductive completeness. This is a requirement on derivability, namely, the principle that in a formal system with material implication and modus ponens, if Y is provable from the hypothesis X, then there is also a proof of X → Y.[6]"

-- https://en.wikipedia.org/wiki/Curry%27s_paradox#Consequences_for_some_formal_logic

Thanks for bringing it up.

[Peter Percival]

Peter Percival wrote:
> Dan Christensen wrote:
>> Can Curry's Paradox be stated in propositional logic as follows:
>>
>>      [A <=> [A => B]] => B
>>
>> This is a tautology.
>
> No.  See https://en.wikipedia.org/wiki/Curry's_paradox#Sentential_logic.

I sent this before I meant to. I wanted to say the title of subsection
2.1 is misleading because ":=" is not a connective of sentential logic
(a fortiori, it isn't <=>). Later on in that section "=" is used in the
role that ":=" was used before, but the same remark applies.

[burs...@gmail.com]

Especially since the curry paradox holds in
LM, which is a paraconsistent and a paracomplete
logic, it also holds in all stronger logics,

LM |- Curry & LM =< Lx => Lx |- Curry

In LM (minimal logic) we can prove Aristoteles
~(p /\ ~p). Here is a proof, we use
~p := p -> F:

------ (Id) ------ (Id)
p |- p F |- F
-----------------
p, p -> F |- F
------------------- (/\L)
p /\ (p -> F) |- F
------------------------ (->R)
|- (p /\ (p -> F)) -> F

But in LM we cannot prove F -> p, hence it
is paraconsistent. And in LM we cannot prove
((p -> F) -> p) -> p, hence it is paracomplete.

[burs...@gmail.com]

LM, minimal logic doesnt have excluded middle from
Aristoteles, but it has identity p -> p from
Aristoteles and non-contradiction ~(p /\ ~p),

as we just saw. LM is deductive complete, it
has even a direct inference rule for that,
which it shares with residuated lattice logics:

G, A |- B
---------
G |- A -> B

Modus ponens is just the inverse of that,
but can be also cast as follows, see Gentzen
cut elimination:

G |- A G, B |- C
--------------------
G, A -> B |- C

An impasse would be, if we could not do
FOL or PROP anymore. But this is not the case,
see also here:

SYSTEMS OF ILLATIVE COMBINATORY LOGIC
COMPLETE FOR FIRST-ORDER PROPOSITIONAL
AND PREDICATE CALCULUS
HENK BARENDREGT, MARTIN BUNDER, AND WIL DEKKERS
THE JOURNALOF SYMBOLIC LOGIC Volume 58, Number 3, Sept. 1993
https://pdfs.semanticscholar.org/1f4c/1862863c28364359bce4fca17e564d5676ed.pdf

The situation is the same with Russel and
Frege, which was fixed in ZFC. But if your
name is fruit cake, and if you live in some

EVER YESTERDAY LAND, and have nothing else
in your space filling curve between your ears
than posting word salad, then of course,

you believe even some wikipedia nonsense.

[burs...@gmail.com]

The Barendregt Paper has in 1.4.PROPOSITION.
A proof of the Curry Paradox. He does it
a way so that he has:

|-_red X

He can use that combinatorically, by some
lambda calculus reduction rules _red, applying
them in both direction, he has Y = Y -> X.

But in propositional logic, we can simulate
what the reduction rules do, and simply try
what Dan tries to do, namely try to obtain a proof:

Y <-> (Y -> X) |- X

The propositional proof will not look very
different to the reduction rules proof, except
that a reduction Y = Y -> X, used in the direction

from Y to Y -> X will propositionally use Y -> (Y->X)
and a reduction Y = Y -> X, used in the direction
from Y -> X to Y will propositionally use (Y->X)->Y,

which is both contained in the equality <->.

[burs...@gmail.com]

Maybe the difference between Russel/Frege and
the ZFC solution then, is that for the Curry
Paradox, especially the reduction based,

what needs to be banned is this self application
that is used in the Y:

lambda y.(yy)

the usualy way is to use some typed lambda calculus
and forbid self application.

But some logicians have ignored the self application
aspect, and started studying the propositional variant.
Check Greg Restall for example.

But besides the lambda and propositional flavor
of the curry paradox, there is of course also the
modal flavor of the curry paradox...

[Ross A. Finlayson]

I quite well respect Curry,
and Burse might be a genius,
and Barendregt et al. are well
known for comprehensive
systems of type.

(Eg Coquand, Luo, Peirce.)

The abstract of "Systems of illatory
logic complete for first order systems
propositional and predicate calculus"
is quite ambitious.

"...The paper fulfills the program of Church [1932],
[1933] and Curry [1930] to base logic on a consistent
system of A-terms or combinators. Hitherto this
program had failed because systems of ICL were
either too weak (to provide a sound interpretation)
or too strong (sometimes even inconsistent)."

I'd that Homotopy Type Theory, with its,
"strength of ZFC and two large cardinals",
is quite directly a rip-off of it, or so derivable.

I never even knew the word "illative" before today.

( https://www.youtube.com/watch?v=3ZKq2ptu7qw )

"In the work of Seldin and others L is defined
as FEH, where E is a universal class. Under this
definition Hp and L(Kp) are interderivable,
but our proof of Proposition 3.10 fails."

I wonder where you might note in this paper
the relevant type theory analog of set theory's
"forcing", applied.

I'm looking at definition 2.12 at it looks like
the introduction of "infinite union" over
regular set theory's usual "pairwise union",
and there you go.

( https://www.youtube.com/watch?v=2Abk1jAONjw )

[burs...@gmail.com]

Its only a paper that shows how to avoid
self application in a formal system.
You get that already in simple types,
nothing about large cardinals or forcing.

https://ncatlab.org/nlab/show/simple+type+theory

In simple type theory you would inductively
define types: some primitive types and then
if p and q are simple types, so is also
p -> q a simple type. The minimal and regular

such set, similar minimality as in Zermelos Z_0
and regularity in set theory, then gives you
something where you cannot have on for a type
(I guess, occurs check in Prolog):

p = .... p .....

As a result when y has a type, self application
(yy) wont be possible anymore. But the Barendregt
Paper might use something else than simple types,
not sure. On the other hand for FOL you don't

need much types, simple types are already enough,
I guess Church might have known that already. For
FOL you only need two primitive types:

o : Propositions

i : Individuals

A function symbol f , is then f : i -> .. -> i -> i,
and a predicate symbol p , is then p : i -> .. -> i -> o,
and connectives are as follows:

F : o

=> : o -> o -> o

forall : (i -> o) -> o

[Ross A. Finlayson]

Set, category, and type theories
are equi-interpretable, right.

Then also there's building types in sets
and classes about categories and so on.

Reflecting on Zermelo's regularity
sees them about the same "strenf"
(which is very great).

[Peter Percival]

Ross A. Finlayson wrote:


> Set, category, and type theories
> are equi-interpretable, right.

?

[Ross A. Finlayson]

The "strength" of those theories and
the space of their theorems are
the same, right.

As fundamental objects:
sets are defined by their elements,
their elements are the relation established by the set
categories are types,
their relations have each category being its own domain ("universe")
types are defined as relations above sets or categories,
establishing equivalence classes of members under relations.

Then, homotopy type theory basically has
"classes are categories", and has the
"strength" of "ZFC plus two measurable
cardinals", or so.

Set theory here is yet "most fundamental", but, the
content or "strength" of set, category, type theories
are equi-interpretable, pretty much the same.

No?

[Peter Percival]

Ross A. Finlayson wrote:
> On Friday, June 29, 2018 at 5:26:02 PM UTC-7, Peter Percival wrote:
>> Ross A. Finlayson wrote:
>>
>>
>>> Set, category, and type theories
>>> are equi-interpretable, right.
>>
>> ?
>
> The "strength" of those theories and
> the space of their theorems are
> the same, right.

What theories? There is more than one set theory and there is more than
one type theory. As for category theory, I know nothing about it. But
I do know, or I think I do, that the logic of a topos is intuitionistic
set theory.

>
> As fundamental objects:
> sets are defined by their elements,
> their elements are the relation established by the set
> categories are types,
> their relations have each category being its own domain ("universe")
> types are defined as relations above sets or categories,
> establishing equivalence classes of members under relations.
>
> Then, homotopy type theory basically has
> "classes are categories", and has the
> "strength" of "ZFC plus two measurable
> cardinals", or so.
>
> Set theory here is yet "most fundamental", but, the
> content or "strength" of set, category, type theories
> are equi-interpretable, pretty much the same.

There you go again.

>
> No?
>
>
>
>
>

[Ross A. Finlayson]

"All of them" is rather the notion that
all those structures are just expressed
relations, that for any set theory there's
a category theory with the same content,
and that types can be built in set or
category theories, including "set" type
and "category" type.

That's not to say that all set theories
are equi-interpretable, of course not,
just that "set theory" and "category
theory" can each result in the same
content all the other can provide.

I wouldn't be surprised if there was
some conclusion of "no empty domains"
or some other limit of the set-builder
or category-builder, I'd be interested
to know about it, but otherwise "set
theory" is from the era of formalization
and "category theory" for its convenience
in building type theories.


Then, the idea about Barendregt et al.'s paper
and not having read it all hope I've read
the relevant noted section correctly, it's
stronger than "regular set theory" to take
"infinite union" besides "pairwise union",
i.e. it's unavailable to regular set theory
_because of_ regularity itself and otherwise
pulling together the deductive result of the
infinite union, so, it comes across as just
like homotopy type theory's axioms which
establish "the strength of" ("the content of")
"ZFC and two large cardinals" for "univalency",
which provides means to derive separately
contradictory results from the same axiom
set (just not, "together", because that
wouldn't be consistent).


Then if I've misread that about the illative
type theory I'd hope to apologize and read
further into it, to apologize here meaning
to explain correctly, for apologetics, but
it seems the theme of binding together
finite combinatorics and regular cardinals
and a universe of type-theoretic universes
on top, these days, just adding more "restriction
of comprehension" or "roundabout mistakes" in
the derivation rules instead of a simpler
foundation built from underneath.

For, it's a quite strong claim, the abstract.

[Dan Christensen]

On Friday, June 29, 2018 at 5:35:10 PM UTC-4, burs...@gmail.com wrote:

> Am Freitag, 29. Juni 2018 22:57:05 UTC+2 schrieb Dan Christensen:
> > On Friday, June 29, 2018 at 3:59:28 PM UTC-4, burs...@gmail.com wrote:
> > > Thus paraconsistent
> > > logics can still be vulnerable to this
> > > paradox, even if they are immune to
> > > the liar paradox.
> >
> > A case of the cure being worse than the supposed "disease?"
> >
> >

> Lets say Lx is one of the logics, LM, LE, etc..
> that Curry considered. And lets say LK is the
> classical logic.
>
> Among the Lx are also some paraconsistent one,
> without ex-falso-quodlibet, etc.. Hence being
> sub intuitionistic.
>
> But the way Curry has set up everything, its
> easy to see, that:
>
> Lx |- A => LK |- A
>
> So what is valid in some of the weaker, maybe
> also paraconsistent logics,
>
> is also valid in classical logic. Quiz, so
> why would one study a family of
>
> systems Lx? Why is there the area of non-classical
> logics in mathematical logic?
>

I can only speculate. It truly is a puzzlement.


Dan

[burs...@gmail.com]

It is the formal support of some philosophical logic.
https://en.wikipedia.org/wiki/Philosophical_logic

Not what fruit cake is positing, more serious
stuff. You need to question the primitivity of
FOL, if you try to do natural language processing,

artificial intelligence, etc... FOL is very
primitiv, it uses only classical logic, and has only
a first order model signatures and quantifiers.

HTT (Homotopy Type Theory) so far, didn't have
much impact on philosophical logic. Except there
somebody also named Dan (J. Daniel) Christensen,

who is Managing Editor of Homology,
Homotopy and Applications.
https://jdc.math.uwo.ca/

But so far there was no explosion of HTT
applications in natural language processing,
aritificial intelligence, etc..

On the other hand lambda calculus had some
impact, like Montague Grammars, Automated
Theorem Proving, etc.. etc..

[Dan Christensen]

On Saturday, June 30, 2018 at 5:39:31 AM UTC-4, burs...@gmail.com wrote:
> Am Samstag, 30. Juni 2018 05:45:55 UTC+2 schrieb Dan Christensen:
> > > systems Lx? Why is there the area of non-classical
> > > logics in mathematical logic?
> > I can only speculate. It truly is a puzzlement.

That was a bit flippant. In my admittedly limited experience as an amateur, I haven't seen any pressing need in mathematics for any system of logic other than the classical form, interesting though they may be in themselves.

> It is the formal support of some philosophical logic.
> https://en.wikipedia.org/wiki/Philosophical_logic
>
> Not what fruit cake is positing, more serious
> stuff. You need to question the primitivity of
> FOL, if you try to do natural language processing,
>
> artificial intelligence, etc... FOL is very
> primitiv, it uses only classical logic, and has only
> a first order model signatures and quantifiers.
>
> HTT (Homotopy Type Theory) so far, didn't have
> much impact on philosophical logic. Except there
> somebody also named Dan (J. Daniel) Christensen,
>

Obviously not me. One of the trolls in another online forum is convinced it is me. He also believes that the universe is just one gigantic plutonium atom. I think you may know of him.

[burs...@gmail.com]

Logic is not only used in mathematics. This
news group is sci.logic, not sci.logic-for-math.
Also the point of Curry, is not to deviate
from classical logic. A weaker logic is not

a deviation. You are halucinating and confused,
I was never talking about deviant logics.

Its only a weaker logic, which you can use
for this mathematics, which only needs weaker
logic. The theorems are still classically valid.
Thats what I showed you, but you cannot read it:

Lx |- A => LK |- A

But I can phrase it for you:

A theorem A in one of the weaker logics,
Lx |- A, is also a theorem in classical
logic, LK |- A.

Everything you can prove in the Curry weaker
logics is classically valid. Nothing deviant
from classical logic. Its not that we try here
to model John Gabriel or WMs brain.

Its still classical, only weaker. Why should
we do that? Well you can figure out yourself.
Should I give you some hints we this is of
interest, or can you figure it out yourself?

Well I give you a hint:
- Assume the theorems of Lx have a certain form,
which you would see in the theorem that you
are about to prove in LK, then your theorem

prover, also a DC proof tool, could switch
to Lx, and still produce a classical proof,
except that maybe Lx has some features, which

make it easer to construct or find a proof.

[burs...@gmail.com]

Here is a very trivial example of such a logic
Lx which is weaker than LK. Hornclauses, so
basically if you have a proving problem:

|- (H1 /\ .. /\ Hn) -> G

Where H1 is a Horn clause, and G is a Horn goal
then you can run it through Prolog and it will
produce a classical valid proof (under the hood,
there are methods to extract it).

Example 1:

|- ((p <- q) /\ q) -> p.

How do you prove it in DC Proof? Can you please
show us a proof? Alternatively you can run this
Prolog program, it will also tell you that it
is provable (I am making this example not because

of proof search, but because of non-classical logic):

Welcome to SWI-Prolog (threaded, 64 bits, version 7.7.1)
SWI-Prolog comes with ABSOLUTELY NO WARRANTY. This is free software.

?- [user].
p :- q.
q.

?- p.
true.

Example 2:
|- (...) -> Basel Problem

I am working on it. Some constructive mathematics
can be also viewed as weaker classical logic. The
result is still classically valid. Only it easier
to deal sometimes. But for the Euler Problem,

I am not yet sure what is needed and how this works out.
But DC Proof has also not yet proved much of mathematics.
There is no Euler Problem example for DC Proof, that
would show that pi^2/6 = lim n->oo sum_i=1^n 1/n^2.

[burs...@gmail.com]

Maybe you are a village idiot Dan, made a DC
proof tool, but doesn't know what he did.

Just assume you disable a few menu items in your
system, eh voila you have a non-classical logic.

Its really that easy.

[burs...@gmail.com]

The problem with non-classical logics is only
that the model theory is a little bit more
complicated, if you disable a few menu items,

but if you want to see the set of consequences
still tight to some valuation, you need non-boolean
valuations. A general method to create

such valuations from the proof theoretic aspect
of a given system, if such a aspect is available,
is the Lindenbaum Algebra:

https://www.encyclopediaofmath.org/index.php/Lindenbaum_method

Welcome to logic...

[burs...@gmail.com]

Another approach to non-classical logic is
via the route of modal logic. So if you disable
a few menu items in your DC proof, you

can view the result as a logic with a weaker
implication for example, and then think about
the implication as a short hand for a modal

form namely you then think about some non-classical
implication ~> as based on a classical implication
-> and a modal operator:

A ~> B :<=> [](A -> B)

Using this view of (some) non-classical logics, you
get the other flavor of curry paradox.

Welcome to logic...

[burs...@gmail.com]

But by choosing curry paradox, you have found
something that will not help you in your quest
to justify classical logic, by meandering

around truth table rows and viewing them as
this and that propositional tautology, and hence
somehow evident. At least the curry paradox

is not specific to classical logic. It doesn't
convey aspects of classical consistency and
completeness, since you can even prove it in

a paraconsistent and paracomplete logic...

Ha Ha

[Dan Christensen]

On Saturday, June 30, 2018 at 7:41:17 AM UTC-4, burs...@gmail.com wrote:
> Am Samstag, 30. Juni 2018 13:21:13 UTC+2 schrieb Dan Christensen:
> > On Saturday, June 30, 2018 at 5:39:31 AM UTC-4, burs...@gmail.com wrote:
> > > Am Samstag, 30. Juni 2018 05:45:55 UTC+2 schrieb Dan Christensen:
> > > > > systems Lx? Why is there the area of non-classical
> > > > > logics in mathematical logic?
> > > > I can only speculate. It truly is a puzzlement.
> >
> > That was a bit flippant. In my admittedly limited experience as an amateur, I haven't seen any pressing need in mathematics for any system of logic other than the classical form, interesting though they may be in themselves.
> >
> >
> > > It is the formal support of some philosophical logic.
> > > https://en.wikipedia.org/wiki/Philosophical_logic
> > >
> > > Not what fruit cake is positing, more serious
> > > stuff. You need to question the primitivity of
> > > FOL, if you try to do natural language processing,
> > >
> > > artificial intelligence, etc... FOL is very
> > > primitiv, it uses only classical logic, and has only
> > > a first order model signatures and quantifiers.
> > >
> > > HTT (Homotopy Type Theory) so far, didn't have
> > > much impact on philosophical logic. Except there
> > > somebody also named Dan (J. Daniel) Christensen,
> > >
> >
> > Obviously not me. One of the trolls in another online forum is convinced it is me. He also believes that the universe is just one gigantic plutonium atom. I think you may know of him.
> >
> >

> Logic is not only used in mathematics.

My main area of interest is the implicit logic the is actually used by mathematicians in writing proofs; not be be confused with the branch of philosophy called mathematical logic.

> This
> news group is sci.logic, not sci.logic-for-math.
> Also the point of Curry, is not to deviate
> from classical logic. A weaker logic is not
>
> a deviation.

While disallowing the application of certain rules of classical logic may be an interesting academic exercise, I don't really see the point. To me, it's a bit like taking away some of a carpenter's tools just to see if he/she can still build a house with the remaining tools.

I can see that certain applications may not require full-blown FOL to write certain classes of proofs, but it's hard to be believe that you can do more with fewer tools.

[burs...@gmail.com]

I didn't say do more. Where did you see me

write "do more"? I only wrote:

Lx |- A => LK |- A

I can phrase it for you once again:

A theorem A in one of the weaker logics,
Lx |- A, is also a theorem in classical
logic, LK |- A.

With your attitude Dan, your are fishing
in the gloomy, maybe for the next 10 years.
I cannot help you,

if somebody is stubborn, he will probably
stay stubborn all his life. There was this
post about Cantorism,

and this Feferman paper, which explained
that not full of ZFC is needed for analysis
etc.. etc..

It is not wise to light a cigarette with
a flamethrower. Most of these theorem provers
that just pick FOL and ZFC,

are nothing more than primitive assemblers,
not apt for practical use...

[Dan Christensen]

On Saturday, June 30, 2018 at 8:45:36 AM UTC-4, burs...@gmail.com wrote:
> Am Samstag, 30. Juni 2018 14:35:02 UTC+2 schrieb Dan Christensen:
> > I can see that certain applications may not require full-blown FOL to write certain classes of proofs, but it's hard to be believe that you can do more with fewer tools.

> I didn't say do more. Where did you see me
> write "do more"?

You suggested that, by using fewer tools, it would "make it easier to construct or find a proof."

Is that not what you meant?

> I only wrote:
>
> Lx |- A => LK |- A
>
> I can phrase it for you once again:
>
> A theorem A in one of the weaker logics,
> Lx |- A, is also a theorem in classical
> logic, LK |- A.
>
> With your attitude Dan, your are fishing
> in the gloomy, maybe for the next 10 years.
> I cannot help you,
>
> if somebody is stubborn, he will probably
> stay stubborn all his life. There was this
> post about Cantorism,
>
> and this Feferman paper, which explained
> that not full of ZFC is needed for analysis
> etc.. etc..
>

I myself don't understand why each of the ZFC axioms (or standard FOL) would be necessary to do classical analysis. I don't have anything like the Axioms of Infinity or Regularity in my set theory, but users could insert additional axioms at the beginning of any proof.

[burs...@gmail.com]

Actually its more tools(*) not fewer tools. Leaving
behind primitive assemblers and trying to use more
advanced tools is more tools, and not fewer tools.

FOL and ZFC is like a primitive assembler. Lets
say its the DNA that controls the production
of proteins in each organism.

But what are the organisms. How can we reach
a further level of evolution in proof tools,
that would really allow building houses.

You cannot build houses with DC Proof. Show
me a proof of this one:

1^n + 2^n + .. + n^n
lim n->oo -------------------- = 1 - 1/e
n^1 + n^2 + .. + n^n

I tried some CAS over the last days, none could
do it automatically. A human can easily do it:

https://www.youtube.com/watch?v=nPNB26hxLPc

Which tool allows doing it easily and rigorously?

(*)
Incorporating results from non-classical logic
into a tool enlarges the tool. Here is a an
example prover that combines Horn with general

Clauses to get a classical prover, which is
complete. The idea is very easy, its not interesting
that it is implemented in Prolog, its only

interesting how a prover can detect subproblems
from non-classical logics, and take advantage
of it, even if the whole problem is not non-classical,

the paper is from 1988:
https://www.researchgate.net/publication/44790956_SATCHMO_a_theorem_prover_implemented_in_Prolog

[burs...@gmail.com]

Corr.:
Organism --> Cells

Now that we have a DNA, what are the Cells?

[Dan Christensen]

> Actually its more tools(*) not fewer tools. Leaving
> behind primitive assemblers and trying to use more
> advanced tools is more tools, and not fewer tools.
>
> FOL and ZFC is like a primitive assembler. Lets
> say its the DNA that controls the production
> of proteins in each organism.
>

I will continue using classical logic and set theory until some other some other systems replace them most math textbooks.

> But what are the organisms. How can we reach
> a further level of evolution in proof tools,
> that would really allow building houses.
>
> You cannot build houses with DC Proof.

You can used it to build solid foundations.

> Show
> me a proof of this one:
>
> 1^n + 2^n + .. + n^n
> lim n->oo -------------------- = 1 - 1/e
> n^1 + n^2 + .. + n^n
>
> I tried some CAS over the last days, none could
> do it automatically. A human can easily do it:
>

Informal proofs are usually much easier for humans to read and write. Computers can't handle informal proofs. It does take humans many years of practice to be able to easily read and write proofs like this, however. And even then, errors can easily occur. A formal proof -- the only kind that computers can do -- is probably out of the question even for this equality. A human would quickly get lost in the mass of details of a formal proof, but the proof will almost certainly be correct.

> https://www.youtube.com/watch?v=nPNB26hxLPc
>
> Which tool allows doing it easily and rigorously?
>

For such applications, you probably want symbolic computing software like Mathematica or Maple. (Not sure since I haven't used them myself.)

[burs...@gmail.com]

Weak classical logic systems are also classical logic.
Even intuitionistic logic entails classical logic.

Whats wrong with you?

But if you have a problem that is an instance of a
fragment, why use cannons to shoot sparrows?
Lets say you have a problem posed to DC proof,
and its already solvable in intuitionistic

logic. What happens with such a proof?

Well its also a classical proof, the same
intuituionistic proof is also a classical
proof. Intuitionistic logic LJ is one of
the many non-classical logics Lx, and

you also have:

LJ |- A => LK |- A

So if the A you want to prove, has some features
that tell a proof tool, that it can
already solve the problem by using LJ only,
I will be damned, if a proof tool

and that cannot detect this and help me in
any way, that such a proof tool can build houses.
Its just a stupid proof tool. For example
this here, this theorem:

|- ((p->q) /\ p) -> q

Can be also proved intuitionistically.
Should be easy to detect for a proof system
such fragements and then help the enduser more
than offer stupid click click click...

Another example would be a proof:

|- 29^29 = 2567686153161211134561828214731016126483469

Do you want the end-user to click 29^29
times, to get the result. What would you
do about it?

[burs...@gmail.com]

Proving things like 2+2=4 only needs intuitionistic
logic. You don't need classical logic for that.

You can check yourself:

add(0,X,X) /* Horn Clause */
add(s(X),Y,s(Z)) <- add(X,Y,Z) /* Horn Clause */

?- add(s(s(n)),s(s(n)),s(s(s(s(n))))). /* Horn Goal */

No LEM used. So why post 2+2=4 as an example of theorem
proving in classical logic. It even doesn't use LEM.

[Ross A. Finlayson]

On Saturday, June 30, 2018 at 5:04:22 AM UTC-7, burs...@gmail.com wrote:
>
> Welcome to logic...
>

Welcome to, "the" logic?

[Peter Percival]

burs...@gmail.com wrote:


> You cannot build houses with DC Proof. Show
> me a proof of this one:
>
> 1^n + 2^n + .. + n^n
> lim n->oo -------------------- = 1 - 1/e
> n^1 + n^2 + .. + n^n
>
> I tried some CAS over the last days, none could
> do it automatically. A human can easily do it:
>
> https://www.youtube.com/watch?v=nPNB26hxLPc

In dealing with the denominator, does he assume that the limit of a sum
is the sum of the limits?

[Dan Christensen]

On Saturday, June 30, 2018 at 12:07:40 PM UTC-4, burs...@gmail.com wrote:
> Am Samstag, 30. Juni 2018 17:56:25 UTC+2 schrieb Dan Christensen:

> > Informal proofs are usually much easier for humans to read and write. Computers can't handle informal proofs. It does take humans many years of practice to be able to easily read and write proofs like this, however. And even then, errors can easily occur. A formal proof -- the only kind that computers can do -- is probably out of the question even for this equality. A human would quickly get lost in the mass of details of a formal proof, but the proof will almost certainly be correct.
> >
> >
> > > https://www.youtube.com/watch?v=nPNB26hxLPc
> > >
> > > Which tool allows doing it easily and rigorously?
> > >
> >
> > For such applications, you probably want symbolic computing software like Mathematica or Maple. (Not sure since I haven't used them myself.)
> >

> Weak classical logic systems are also classical logic.
> Even intuitionistic logic entails classical logic.
>

So, what?

[snip]

>
> Another example would be a proof:
>
> |- 29^29 = 2567686153161211134561828214731016126483469
>
> Do you want the end-user to click 29^29
> times, to get the result. What would you
> do about it?
>

I would use special-purpose software to do such calculations. You certainly wouldn't write a formal proof.

You might, for example, use formal proofs to establish the existence of the ^ operator on N to make sure it is on solid foundation and that your axioms and rules of inference are adequate for the tasks at hand. You could justify leaving 0^0 undefined (or whatever).

[burs...@gmail.com]

He might have use a method that is not generally
valid, but nevertheless obtained a correct result.

How would a theorem prover based proof look like?
BTW: Numerical, you can check yourself,

the 1-1/e is plausible.

[j4n bur53]

Nope, its studies in logic. But on the other
hand your are right, its "the" fruit cake,

and its "the" word salad. But it seems that
more en vogue is "formal logic" now:

Fathoming Formal Logic: Vol I
Theory and Decision Procedures for Propositional Logic
Odysseus Makridis

Anybody a PDF with table of contents?
Its from february 2018 and not very expensive.

Ross A. Finlayson schrieb:

[j4n bur53]

You can also solve:

4-x^2
----- = 3
2-x

by cancelling. Only this one goes wrong:

4-x^2
----- = 4
2-x


burs...@gmail.com schrieb:

[burs...@gmail.com]

There is no strict line that you can draw between
proof and calculation. A proof might need calculation
from time to time. Otherwise you cannot build houses.

You want a solid house, not some tent. You want that
the house has everything walls, roof, etc.. Delegating
to another tool might be a solution,

but it would also show that there is a gap somewhere in
your system, that it cannot combine the two.

[j4n bur53]

At least FOL and ZFC doesn't draw a line between
the two. Its the same DNA that drives a calculation

cell and that drives a more abstract proof cell.
Also a calculation cell might yield a result

which is not good old arithmetic, it could
return 1723+n^2 for example, and the polynomial

itself would be a result of some "calculation"
and this polynomial would be later used in a proof.

burs...@gmail.com schrieb:

[Ross A. Finlayson]

So, it's equi-interpretable, your working theory,
with any number of other theories?

Or, just the one?

[Dan Christensen]

On Saturday, June 30, 2018 at 12:55:44 PM UTC-4, burs...@gmail.com wrote:
> Am Samstag, 30. Juni 2018 18:36:14 UTC+2 schrieb Dan Christensen:

> >
> There is no strict line that you can draw between
> proof and calculation.

On the contrary, with a formal proof, you must show all the intermediate results. A calculator is block box. A calculator does not usually show any intermediate results.

> A proof might need calculation
> from time to time.

Only in an informal proof. There is no calculator function in the FOL or ZFC axioms.

> You want a solid house, not some tent. You want that
> the house has everything walls, roof, etc.. Delegating
> to another tool might be a solution,
>
> but it would also show that there is a gap somewhere in
> your system, that it cannot combine the two.
>

There is no theoretical "gap." If you to prove that 2+2=4, DC Proof is more than adequate for the job. If you want to prove 29^29 = 2567686153161211134561828214731016126483469, there is probably not a computer on the planet that would big enough to be able to display all the intermediate steps of proof.

[j4n bur53]

Logic is not a theory. FOL is a logic.
But ZFC is a theory formulated in the
logic of FOL.

What are you talking about fruit cake?
Some word salad I guess. Chance that any
makes sense when you posts

are nearly zero.

FOL when viewed as a calculus, that
recursively enumerates the consequences,
has different incarnations,

NK natural deduction, LK sequent calculus,
HK hilbert style. Each of these incarnations
may contain non-classical logics.

In the Gentzen paper about cut-elimation,
you find already mentioned LJ. But the
idea is not to use some double negation

translation, and run LK in LJ. Its more
a theorem prover like DC Proof, should
detect fragments and offer

a richer tooling.

[j4n bur53]

Because there is no harm in producing
non-classical logic proofs, if they are
not deviant, you have:

Lx |- A => LK |- A

The L is for sequent calculus. The
above is **not** an equi-interpretation.
Its based on very simple

thinks like for example LK=Lx+something,
and then its evident by montonicity,
that the above holds.

https://en.wikipedia.org/wiki/Monotonicity_of_entailment

Non-deviant non-classical logics are
typically monotonic like classical
logic itself.

j4n bur53 schrieb:

[burs...@gmail.com]

There are only log2(29) steps for power
itself, if you use the usual binary power algorithm.

Then there are some steps for the involved multiplication.
You could do it like metamath:

http://at.metamath.org/mpegif/df-dec.html

[burs...@gmail.com]

Description: Example for df-dec 10339, 1000 + 2000 = 3000.

This proof disproves (by counter-example) the
assertion of Hao Wang, who stated, "There is
a theorem in the primitive notation of set
theory that corresponds to the arithmetic
theorem 1000 + 2000 = 3000. The formula
would be forbiddingly long... even if
(one) knows the definitions and is asked
to simplify the long formula according
to them, chances are he will make errors
and arrive at some incorrect result." (Hao
Wang, "Theory and practice in mathematics" ,
In Thomas Tymoczko, editor, New Directions
in the Philosophy of Mathematics, pp 129-152,
Birkauser Boston, Inc., Boston, 1986.
(QA8.6.N48). The quote itself is on page 140.)

http://at.metamath.org/mpegif/1kp2ke3k.html

[FredJeffries]

On Saturday, June 30, 2018 at 8:56:25 AM UTC-7, Dan Christensen wrote:

> I will continue using classical logic and set theory until some other some other systems replace them most math textbooks.

Math textbooks do not use "classical logic and set theory", as you yourself state below,

> > But what are the organisms. How can we reach
> > a further level of evolution in proof tools,
> > that would really allow building houses.
> >
> > You cannot build houses with DC Proof.
>
> You can used it to build solid foundations.
>
>
> > Show
> > me a proof of this one:
> >
> > 1^n + 2^n + .. + n^n
> > lim n->oo -------------------- = 1 - 1/e
> > n^1 + n^2 + .. + n^n
> >
> > I tried some CAS over the last days, none could
> > do it automatically. A human can easily do it:
> >
>
> Informal proofs are usually much easier for humans to read and write.

Indeed. Even textbooks on formal logic do not USE formal logic.

[Dan Christensen]

On Saturday, June 30, 2018 at 3:28:21 PM UTC-4, FredJeffries wrote:
> On Saturday, June 30, 2018 at 8:56:25 AM UTC-7, Dan Christensen wrote:
>
> > I will continue using classical logic and set theory until some other some other systems replace them most math textbooks.
>
> Math textbooks do not use "classical logic and set theory", as you yourself state below,

OMG! What aspect of ordinary logic and set theory do you think is NOT used in math textbooks? Last I looked, they STILL had proofs by contradiction, power sets, arbitrary subsets and the like.

[Ross A. Finlayson]

Hmm, no "final cause", no "first principle":
must be classical.

https://en.wikipedia.org/wiki/Monotonicity_of_entailment
https://en.wikipedia.org/wiki/Non-monotonic_logic

I can have "square of opposition" without
"monotonicity of entailment", and it's
neither of a "monotonic" nor "non-monotonic"
logic.

Adding a "useless" stipulation to the antecedent
pretty quickly breaks the logic in the temporal
and things change.

The temporal logic isn't necessarily non-monotonic,
which correctly could be modeled all in classical
syllogisms and also without monotonicity of entailment,
and also that's all still classical.

Science and belief simply have a reasonable
meta-model of the scientific principle and
fallibility of belief, not "it's your turn
to change the logic".

[burs...@gmail.com]

Nobody changes a logic when studying non-standard
logic, especially not in the sense of Haskell Brooks
Curry. You are halucinating and confused.

I guess you dont understand the logic tower
LM, LJ, LK for example. Its just a lattice:

LK
|
LJ
|
LM

What is true in LM, is also true in LK. If
you want to do proofs for LK, you can also
do them in LM. And if you find one in LM
you also have one for LK.

If you don't find a proof in LM, you can
still try LK.

[Ross A. Finlayson]

https://en.wikipedia.org/wiki/Rational_consequence_relation

"If the conclusion seems silly to you
then you might consider replacing
the word soap with the word eggs
to see if it changes your feelings."

That's not fundamental logic,
just gut hunches in the feels.

"If this latter conclusion seems
ridiculous to you then it is likely
that you are subconsciously
asserting your own preconceived knowledge...."

... and were wrong!

This non-monotonicity is "non" in the sense
that it entirely discards invalidated expressions
instead of marking them false. (As in,
the monotonic collection of "that was wrong".)

There's no erase. There's no eraser.
You make a mistake, cross a line through
it and leave it. And fix it.

[j4n bur53]

Again, let me iterate, classical logic is
monotonic, so are its non deviant sub logics.
So if you have a stain on your trouser. You

could first try soap to remove it, lets say
this is the LM logic. And if this is not
working you can still try javel water, lets

say this is LK logic. Here is a using
non-classical logic for dummies:

Start
|
/ Can I prove \____yes
\ it with LM / |
|No |
| |
/ Can I prove \____yes
\ it with LK / |
|No |
| |
No LK proof LK proof

Ross A. Finlayson schrieb:

[j4n bur53]

The below works because of:

LM |- A => LK |- A

j4n bur53 schrieb:

[burs...@gmail.com]

Fruit cake possibly never seen an implication,
from meta/mathematical logic as below.

Now his brains is cooking, trying to find word
salad, already 90% if his brain cells

have evaporated so hot was the cooking.

[Ross A. Finlayson]

https://en.wikipedia.org/wiki/Universal_logic

"Super logic"

[Ross A. Finlayson]

Aren't you a logicist,
and logical positivist,
too or also?

https://en.wikipedia.org/wiki/Logical_positivism

Technical philosophers
are not necessarily
only logical positivists.

And, the position of logical positivism
can be held with yet the extra and super
about that, too.

"Unscientific discourse, as in
ethics and metaphysics, would be
unfit for discourse by philosophers,
newly tasked to organize knowledge,
not develop new knowledge."

Ah, so now they're platonists,
discovering instead of inventing
fact.

Postpositivism isn't fundamental
in foundations, it's not extra-scientific,
it's a retrenchment to gut hunch feels
(and stipulation, i.e., it's non-scientific).

Superpositivism is all scientific
and fundamental, too, and also.

[Ross A. Finlayson]

On Saturday, June 30, 2018 at 1:45:10 PM UTC-7, j4n bur53 wrote:

Classical logic is only monotonic
with no false antecedents.

Otherwise that's real "junk DNA of logic",
which the old central dogma of molecular
biology used to have 85% of the genome as
about, though now the old central dogma of
molecular biology (that is new) has discovered
that pretty much all that is not genetic
garbage or damage.

Paraconsistency is the establishment
about the balance.

[burs...@gmail.com]

Classical logic is always monotonic.
There is no such thing as false antecendent.

If you use a new antecendent which is in
conflict with some existing conclusion,

you get maybe explosion. But under explosion
monotonicity is still preserved. You can check

yourself:

p |- p

p |/- ~p

Now I add ~p:

p, ~p |- p

p, ~p |- ~p

Looks pretty montonic to me. You are confused
and halucinating. You don't understand classical

logic at all.

[burs...@gmail.com]

Monotonicity only says the following:

G |- A => G, B |- A /* that is monotonicity */

https://en.wikipedia.org/wiki/Monotonicity_of_entailment

It doesn't say:

G |/- A => G, B |/- A /* that would not be
called monotonicity of
entailment */

[burs...@gmail.com]

What is anti-monotonic is consistency. You
have the following for theories:

Con(G, A) => Con(G)

[Ross A. Finlayson]

About "|-", turnstile, and "|/-",

"...[T]he combination of Frege's
Urteilsstrich, judgement stroke [ | ], and
Inhaltsstrich, content stroke [—],
came to be called the assertion sign."

What's "|/-"?

And, can you use "->" for direct implication,
instead of "=>" for material implication?

[burs...@gmail.com]

This one is also nice:

!n 1
lim n->oo -- = -
n! e

Source:
https://en.wikipedia.org/wiki/Derangement#Limit_of_ratio_of_derangement_to_permutation_as_n_approaches_%E2%88%9E

Not sure whether there is some immediate
relationship to the other below problem.

Am Samstag, 30. Juni 2018 18:30:54 UTC+2 schrieb Peter Percival:
> burs...@gmail.com wrote:
>
>

> > You cannot build houses with DC Proof. Show

> > me a proof of this one:
> >
> > 1^n + 2^n + .. + n^n
> > lim n->oo -------------------- = 1 - 1/e
> > n^1 + n^2 + .. + n^n
> >
> > I tried some CAS over the last days, none could
> > do it automatically. A human can easily do it:
> >

[burs...@gmail.com]

"|/-" is defined as follows:

G |- A :<=> ~(G |- A)

The choice of "->" or "=>" is irrelevant,
as long as you understand on what level
they happen. I use space around the implication
sign to indicate the level, so the following:

G |- A => G, B |- A

Is read as:

(G |- A) => (G, B |- A)

And hence the => is on the meta level, meta
mathematical logic result. Not part of some
formula on the object level.

[burs...@gmail.com]

Corr.:

G |/- A :<=> ~(G |- A)

[George Greene]

On Friday, June 29, 2018 at 3:20:30 PM UTC-4, Dan Christensen wrote:
> Can Curry's Paradox be stated in propositional logic as follows:
>
> [A <=> [A => B]] => B
>
> This is a tautology.

Well, yeah, but it's also not Curry's Paradox.


Some things sort of have to get separated here.
The assertion of the equivalence is not the same thing
as either of the things being asserted to be equivalent.
You are trying to translate
A: A-> B, but the thing to the left of the comma IS NOT the same
thing as A.
It is TRUE in this scenario THAT
A<=>[A->B], but that must remain true EVEN WHEN A IS FALSE,
so that can't be A.

A->B is the same thing as A, but
A<=>[A->B] is not the same thing as A.
P<->P is not the same thing as P.

[George Greene]

On Friday, June 29, 2018 at 3:31:59 PM UTC-4, burs...@gmail.com wrote:
> You need less than classical logic, to deduce Curry's
> paradox. Thats why it is a paradox.

How is any of that even relevant? ISn't the prior question whether one has
OR HAS NOT TRANSLATED Curry's paradox into classical propositional logic
*C*O*R*R*E*C*T*L*Y*??
"If this sentence is true" CANNOT BE SAID in classical logic -- classical
logic does NOT HAVE labels.
You can ATTACH labels if you like, but
but then the usual mode of translation turns
an instanec of Curry's Paradox into an instance of
A: A->B ,
WHICH IS NOT paradoxical in classical logic -- it is just equivalent
to A/\B .

[burs...@gmail.com]

A<->(A->B), is equivalent to A/\B, in
classical logic.

A B ((A ↔ (A → B)) ↔ (A ∧ B))
F F T
F T T
T F T
T T T
http://web.stanford.edu/class/cs103/tools/truth-table-tool/

So you still get the same A/\B -> B.

A B ((A ∧ B) → B)
F F T
F T T
T F T
T T T
http://web.stanford.edu/class/cs103/tools/truth-table-tool/

Thats another way of proving (A<->(A->B))->B.
But whats your point?

[burs...@gmail.com]

What I don't know is, whether A<->(A->B)
is also equivalent to A/\B in minimal logic,
some non-classical logic.

If this equivalence doesn't hold in this
non-classical logic, you cannot recreate the
paradox as A/\B -> B.

What holds in non-classical logic, is the
last step, namely, no LEM needed:

---------- (Id)
A,B |- B
-------------
A/\B |- B
-------------
|- A/\B -> B

But for (A<->(A->B))<->(A/\B), can this
be proved without LEM?

[Ross A. Finlayson]

Thanks.

Here "monotonic" seems to be "doesn't break
the derivation rule", but it's not causality,
and "correlation" (of, not breaking the derivation
rule, here with the comma operator and that
implicitly there is still the requirement of
the original derivation rule) is not "causation".

That's:
Cause -> Effect
and not
Cause, (Immaterial) -> Effect
except
Immaterial -> Nothing

So, a monotonic logic just seems to be that
then, given all of its formulae are "consistent",
i.e., their transitive closure of all the judgments
has no derivations of conflicting judgments.

https://en.wikipedia.org/wiki/Sequent_calculus

Then, this notion of paraconsistency in the
context of resolving paradox, then is for
building (or for the platonist, deducing)
why for example there is continuity of motion
but infinite divisibility, and it's not a paradox.

So, monotonicity just seems to reflect
consistent formulae, i.e., it's a property
of the model, that then the logic (or,
collection of derivation rules) are
undisturbed by their free composition.

Then, non-monotonicity might reflect either
"the formulae are inconsistent",
"the derivation rules aren't to be disturbed",
"there's no free composition",
or otherwise not having the satisfactory
properties of "monotonicity".

Then, a "non-monotonic logic" is basically
for a "working set of terms", but, it's not
in a fundamental sense "perfect" (truths,
only and all truths, constant, consistent,
complete, concrete, ...).

And, the monotonic is classical with
eliminating all the non-causal relations,
(for that then some nonstandard, super-classical
fundamental theory has _all_ the relations are
related, consistently, so it's monotonic and
classical too).

[George Greene]

On Friday, June 29, 2018 at 6:41:08 PM UTC-4, j4n bur53 wrote:
> The Barendregt Paper has in 1.4.PROPOSITION.
> A proof of the Curry Paradox. He does it
> a way so that he has:
>
> |-_red X
>
> He can use that combinatorically, by some
> lambda calculus reduction rules _red, applying
> them in both direction, he has Y = Y -> X.
>
> But in propositional logic, we can simulate
> what the reduction rules do, and simply try
> what Dan tries to do, namely try to obtain a proof:
>
> Y <-> (Y -> X) |- X
>
> The propositional proof will not look very
> different to the reduction rules proof, except
> that a reduction Y = Y -> X, used in the direction
>
> from Y to Y -> X will propositionally use Y -> (Y->X)
> and a reduction Y = Y -> X, used in the direction
> from Y -> X to Y will propositionally use (Y->X)->Y,
>
> which is both contained in the equality <->.

Why are you making it so complicated?
Propositionally,
Y <-> [Y->X]
IS EQUIVALENT TO
Y/\X,
SO OF COURSE that implies Y, and implies X.

[Dan Christensen]

On Sunday, July 1, 2018 at 2:28:52 PM UTC-4, George Greene wrote:
> On Friday, June 29, 2018 at 3:20:30 PM UTC-4, Dan Christensen wrote:
> > Can Curry's Paradox be stated in propositional logic as follows:
> >
> > [A <=> [A => B]] => B
> >
> > This is a tautology.
>
> Well, yeah, but it's also not Curry's Paradox.
>
>
> Some things sort of have to get separated here.
> The assertion of the equivalence is not the same thing
> as either of the things being asserted to be equivalent.
> You are trying to translate
> A: A-> B, but the thing to the left of the comma IS NOT the same
> thing as A.

But is it not the same as A <=> [A => B]?

> It is TRUE in this scenario THAT
> A<=>[A->B], but that must remain true EVEN WHEN A IS FALSE,
> so that can't be A.
>

X <=> Y means you can substitute Y for X in any logical statement, regardless of whether X is true or false. Likewise for X : Y. Correct?

> A->B is the same thing as A, but
> A<=>[A->B] is not the same thing as A.
> P<->P is not the same thing as P.

[Peter Percival]

Dan Christensen wrote:
> On Sunday, July 1, 2018 at 2:28:52 PM UTC-4, George Greene wrote:
>> On Friday, June 29, 2018 at 3:20:30 PM UTC-4, Dan Christensen wrote:
>>> Can Curry's Paradox be stated in propositional logic as follows:
>>>
>>> [A <=> [A => B]] => B
>>>
>>> This is a tautology.
>>
>> Well, yeah, but it's also not Curry's Paradox.
>>
>>
>> Some things sort of have to get separated here.
>> The assertion of the equivalence is not the same thing
>> as either of the things being asserted to be equivalent.
>> You are trying to translate
>> A: A-> B, but the thing to the left of the comma IS NOT the same
>> thing as A.
>
> But is it not the same as A <=> [A => B]?

All A <=> [A => B] says is that A and [A => B] have the same
truth-value. Curry's paradox requires A and [A => B] to be (in some
sense) equivalent; unfortunately, not just materially equivalent.

[Dan Christensen]

On Monday, July 2, 2018 at 9:52:48 AM UTC-4, Peter Percival wrote:
> Dan Christensen wrote:
> > On Sunday, July 1, 2018 at 2:28:52 PM UTC-4, George Greene wrote:
> >> On Friday, June 29, 2018 at 3:20:30 PM UTC-4, Dan Christensen wrote:
> >>> Can Curry's Paradox be stated in propositional logic as follows:
> >>>
> >>> [A <=> [A => B]] => B
> >>>
> >>> This is a tautology.
> >>
> >> Well, yeah, but it's also not Curry's Paradox.
> >>
> >>
> >> Some things sort of have to get separated here.
> >> The assertion of the equivalence is not the same thing
> >> as either of the things being asserted to be equivalent.
> >> You are trying to translate
> >> A: A-> B, but the thing to the left of the comma IS NOT the same
> >> thing as A.
> >
> > But is it not the same as A <=> [A => B]?
>
> All A <=> [A => B] says is that A and [A => B] have the same
> truth-value. Curry's paradox requires A and [A => B] to be (in some
> sense) equivalent; unfortunately, not just materially equivalent.
>

What other sense of logical equivalence is there?

[Jim Burns]

On 7/2/2018 9:52 AM, Peter Percival wrote:
> Dan Christensen wrote:
>> On Sunday, July 1, 2018 at 2:28:52 PM UTC-4,
>> George Greene wrote:
>>> On Friday, June 29, 2018 at 3:20:30 PM UTC-4,
>>> Dan Christensen wrote:

>>>> Can Curry's Paradox be stated in propositional logic
>>>> as follows:
>>>> [A <=> [A => B]] => B
>>>> This is a tautology.
>>>
>>> Well, yeah, but it's also not Curry's Paradox.
>>> Some things sort of have to get separated here.
>>> The assertion of the equivalence is not the same thing
>>> as either of the things being asserted to be equivalent.
>>> You are trying to translate
>>> A: A-> B, but the thing to the left of the comma IS NOT
>>> the same thing as A.
>>
>> But is it not the same as A <=> [A => B]?
>
> All A <=> [A => B] says is that A and [A => B] have
> the same truth-value

> Curry's paradox requires A and [A => B] to be (in some
> sense) equivalent; unfortunately, not just materially
> equivalent.

Piggybacking.

What makes the conclusion that B is true so paradoxical is that
we *DON'T* assume the truth of any particular sentence, not
A <-> (A -> B), not A, not A -> B.

We only assume the _existence_ of the Curry sentence A, and
that A is either true or false. B drops out of an empty sky.

Assume A = "A -> B" is either true or false.

(i)
Suppose A is false.
Then A -> B is false, A & ~B is true, A is true.
Contradiction.

(ii)
Suppose A is true.
Then A -> B is true, and by modus ponens, B is true.

----
Consider A <-> (A -> B).
As I see it, this is equivalent to
(A & (A -> B)) \/ (~A & (A & ~B))
or
A & B

Certainly, B _follows_ from A <-> (A -> B)
but I can deny A <-> (A -> B), AKA A & B,
and stay logically consistent.
We don't get that choice with A = "A -> B".

----
The wild cards are that a sentence A = "A - > B" exists and
that A is either true or false. These don't seem so very
controversial (which is what makes it a good paradox).

One way of keeping B from dropping out of an empty sky is
to forbid sentences such as A = "A -> B". And that is a
fair response.

Another way is to look more closely at the assumption that
sentences like A = "A -> B" are true or false. I find the
revision theory of truth RTT to be an interesting take on that.
https://plato.stanford.edu/entries/truth-revision/

I would rather expand the expressiveness of our logical
language than restrict it, so I start out biased in favor
of RTT.

But I also think that dealing with such tangles as A = "~A"
and A = "A -> B" teases out a distinction between language
that may describe the "real world", maybe the class of all
flying rainbow sparkle-ponies, and language that may describe
_language_ , which is not in the real world and may not be
subject to the same rules as the real world.

We do not want language that describes Midnight Sparkle to
be flying and also not flying, because we do not experience
such things. But we don't see the truth of sentences the
way we see Midnight Sparkle in the air -- or not in the air.

I find it very reasonable to approach the truth values of
sentences about sentences -- meta-sentences? -- more carefully.
Perhaps we can derive a Law of Excluded Middle for them,
or for some of them. Or perhaps not. And that is my layman's
view on the revision theory of truth: a more careful approach
to parts of logic that we should not assume we have got
correct.

[Dan Christensen]

In classical logic, from proposition A, we can infer A OR B, B => A and ~A => B regardless of whether A an B are true or false. There is nothing "paradoxical" about it. These are all common used methods of proof that actually work.

[snip]

[Peter Percival]

That rather hints that Curry's paradox can't be expressed in
propositional logic!

[Dan Christensen]

Yeah, it seems if you want to avoid paradoxes, best to stick with classical logic.

[burs...@gmail.com]

Thats the shortest proof I get in
minimal logic sequent calculus:

1: x, x→(x→y), (x→y)→x ⊢ x /* id */
2: x→y, x, (x→y)→x ⊢ x /* id */
3: y, x, (x→y)→x ⊢ y /* id */
4: x→y, x, (x→y)→x ⊢ y /* left 2, 3 */
5: x, x→(x→y), (x→y)→x ⊢ y /* left 1, 4 */
6: x→(x→y), (x→y)→x ⊢ x→y /* right 5 */
7: x, x→(x→y) ⊢ x /* id */
8: x→y, x ⊢ x /* id */
9: y, x ⊢ y /* id */
10: x→y, x ⊢ y /* left 8,9 */
11: x, x→(x→y) ⊢ y /* left 7,10 */
12: x→(x→y),(x→y)→x ⊢ y /* left 6,11 */

The used logic is an implicational fragment,
without any conjunction. But the proof is
also classicaly valid, but the interesting

thing is rather that it can be already performed
in a paraconsistent and paracomplete logic,
such as the above used minimal logic LM.

[burs...@gmail.com]

Its also a classical proof, since the inference
rules and axioms of LM (minimal logic, some
sequent calculus variant of it) are a subset

of the inferenece rules and axioms of LK (classical
logic, some sequent calculus variant). At least
Haskell Brooks Curry and others, like Gentzen

have repeatedly presented variants of axioms
and inference rules, that follow this subset
schema. Therefore we have trivially:

S ⊢LM A => S |-LK A

If a formal system F1 is subset of a formal subset F2,
what concerces inference rules and axioms, then
trivially what can be proved in F1 can also be

proved in F2. This holds only if the axioms and
inference rules are given as, maybe even some
side conditions in the axioms and inference rules:


-------- (some axiom)
A


A1 ... An
--------------------- (some inference rule)
A

[burs...@gmail.com]

What was used for the minimal logic sequent calculus,
where only these axioms and inference rules:

--------- (Id)
G, A |- A

G, A |- B
----------- (Right)
G |- A -> B

G, A -> B, D |- A B, G, D |- C
--------------------------------- (Left)
G, A -> B, D |- C

Due to Dragalin: A less well-known result of
1977 (cf. [6]) concerns the system Dragalin called
the theory of definable sets of natural numbers.

Ha Ha, WM, definable, woa!

The Bulletin of Symbolic Logic
Volume 5, Number 3, Sept. 1999
IN MEMORIAM: ALBERT G. DRAGALIN
1941–1998

[burs...@gmail.com]

Strange thing, if we view set membership as a
kind of application operator, which makes sense,
since for a setlike predicate x in P, is not much

different from P(x). But why is set theory and
theorem provers such as DC Proof, that only
offers set theory hated? Here is a rant

against set theory:

"Set theory is harder to automate than
type theory. It is low-level, with s
trange definitions like ⟨a,b⟩ ≡ {{a},
{a,b}} and 3 ≡ {0,1,2}; and since it
has no information hiding, it admits
strange theorems like {a} ∈ ⟨a, b⟩ and
2 ∈ 3. The search space is larger in
set theory than in type theory: set
theory proofs need extra steps to
perform type checking, and the lack
of type constraints admits more terms
as well-formed. Virtually all type
theories satisfy strong normalization:
every reduction sequence terminates in
a normal form. The corresponding notion
of reduction in set theory, which reduces
t ∈ {x.ψ[x]} to ψ[t], admits expressions
with no normal form [3]. For example,
{x . x ∈ x} ∈ {x . x ∈ x} reduces to
itself [10, page 295]. Type theory
provers rely upon strong normalization; a
set theory prover must do without
this property."

Set Theory for Verification:
I. From Foundations to Functions∗
Lawrence C. Paulson
https://www.cl.cam.ac.uk/~lp15/papers/Formath/set-I.pdf

LoL

Am Samstag, 30. Juni 2018 01:45:54 UTC+2 schrieb j4n bur53:
> Its only a paper that shows how to avoid
> self application in a formal system.
> You get that already in simple types,
> nothing about large cardinals or forcing.
>
> https://ncatlab.org/nlab/show/simple+type+theory
>
> In simple type theory you would inductively
> define types: some primitive types and then
> if p and q are simple types, so is also
> p -> q a simple type. The minimal and regular
>
> such set, similar minimality as in Zermelos Z_0
> and regularity in set theory, then gives you
> something where you cannot have on for a type
> (I guess, occurs check in Prolog):
>
> p = .... p .....
>
> As a result when y has a type, self application
> (yy) wont be possible anymore. But the Barendregt
> Paper might use something else than simple types,
> not sure. On the other hand for FOL you don't
>
> need much types, simple types are already enough,
> I guess Church might have known that already. For
> FOL you only need two primitive types:
>
> o : Propositions
>
> i : Individuals
>
> A function symbol f , is then f : i -> .. -> i -> i,
> and a predicate symbol p , is then p : i -> .. -> i -> o,
> and connectives are as follows:
>
> F : o
>
> => : o -> o -> o
>
> forall : (i -> o) -> o
>
> Am Samstag, 30. Juni 2018 01:22:05 UTC+2 schrieb Ross A. Finlayson:
> > On Friday, June 29, 2018 at 3:31:08 PM UTC-7, burs...@gmail.com wrote:
> > > LM, minimal logic doesnt have excluded middle from
> > > Aristoteles, but it has identity p -> p from
> > > Aristoteles and non-contradiction ~(p /\ ~p),
> > >
> > > as we just saw. LM is deductive complete, it
> > > has even a direct inference rule for that,
> > > which it shares with residuated lattice logics:
> > >
> > > G, A |- B
> > > ---------

> > > G |- A -> B
> > >

> > > Modus ponens is just the inverse of that,
> > > but can be also cast as follows, see Gentzen
> > > cut elimination:
> > >
> > > G |- A G, B |- C
> > > --------------------
> > > G, A -> B |- C
> > >
> > > An impasse would be, if we could not do
> > > FOL or PROP anymore. But this is not the case,
> > > see also here:
> > >
> > > SYSTEMS OF ILLATIVE COMBINATORY LOGIC
> > > COMPLETE FOR FIRST-ORDER PROPOSITIONAL
> > > AND PREDICATE CALCULUS
> > > HENK BARENDREGT, MARTIN BUNDER, AND WIL DEKKERS
> > > THE JOURNALOF SYMBOLIC LOGIC Volume 58, Number 3, Sept. 1993
> > > https://pdfs.semanticscholar.org/1f4c/1862863c28364359bce4fca17e564d5676ed.pdf
> > >
> > > The situation is the same with Russel and
> > > Frege, which was fixed in ZFC. But if your
> > > name is fruit cake, and if you live in some
> > >
> > > EVER YESTERDAY LAND, and have nothing else
> > > in your space filling curve between your ears
> > > than posting word salad, then of course,
> > >
> > > you believe even some wikipedia nonsense.
> > >
> > > Am Samstag, 30. Juni 2018 00:12:49 UTC+2 schrieb burs...@gmail.com:
> > > > Especially since the curry paradox holds in
> > > > LM, which is a paraconsistent and a paracomplete
> > > > logic, it also holds in all stronger logics,
> > > >
> > > > LM |- Curry & LM =< Lx => Lx |- Curry
> > > >
> > > > In LM (minimal logic) we can prove Aristoteles
> > > > ~(p /\ ~p). Here is a proof, we use
> > > > ~p := p -> F:
> > > >
> > > > ------ (Id) ------ (Id)
> > > > p |- p F |- F
> > > > -----------------
> > > > p, p -> F |- F
> > > > ------------------- (/\L)
> > > > p /\ (p -> F) |- F
> > > > ------------------------ (->R)
> > > > |- (p /\ (p -> F)) -> F
> > > >
> > > > But in LM we cannot prove F -> p, hence it
> > > > is paraconsistent. And in LM we cannot prove
> > > > ((p -> F) -> p) -> p, hence it is paracomplete.
> > > >
> > > > Am Freitag, 29. Juni 2018 23:35:10 UTC+2 schrieb burs...@gmail.com:
> > > > > Lets say Lx is one of the logics, LM, LE, etc..
> > > > > that Curry considered. And lets say LK is the
> > > > > classical logic.
> > > > >
> > > > > Among the Lx are also some paraconsistent one,
> > > > > without ex-falso-quodlibet, etc.. Hence being
> > > > > sub intuitionistic.
> > > > >
> > > > > But the way Curry has set up everything, its
> > > > > easy to see, that:
> > > > >
> > > > > Lx |- A => LK |- A
> > > > >
> > > > > So what is valid in some of the weaker, maybe
> > > > > also paraconsistent logics,
> > > > >
> > > > > is also valid in classical logic. Quiz, so
> > > > > why would one study a family of
> > > > >
> > > > > systems Lx? Why is there the area of non-classical
> > > > > logics in mathematical logic?
> > > > >
> > > > > Am Freitag, 29. Juni 2018 22:57:05 UTC+2 schrieb Dan Christensen:
> > > > > > On Friday, June 29, 2018 at 3:59:28 PM UTC-4, burs...@gmail.com wrote:
> > > > > > > Thus paraconsistent
> > > > > > > logics can still be vulnerable to this
> > > > > > > paradox, even if they are immune to
> > > > > > > the liar paradox.
> > > > > >
> > > > > > A case of the cure being worse than the supposed "disease?"
> > > > > >
> > > > > >
> > > > > > Dan
> >
> >
> > I quite well respect Curry,
> > and Burse might be a genius,
> > and Barendregt et al. are well
> > known for comprehensive
> > systems of type.
> >
> > (Eg Coquand, Luo, Peirce.)
> >
> > The abstract of "Systems of illatory
> > logic complete for first order systems
> > propositional and predicate calculus"
> > is quite ambitious.
> >
> > "...The paper fulfills the program of Church [1932],
> > [1933] and Curry [1930] to base logic on a consistent
> > system of A-terms or combinators. Hitherto this
> > program had failed because systems of ICL were
> > either too weak (to provide a sound interpretation)
> > or too strong (sometimes even inconsistent)."
> >
> > I'd that Homotopy Type Theory, with its,
> > "strength of ZFC and two large cardinals",
> > is quite directly a rip-off of it, or so derivable.
> >
> > I never even knew the word "illative" before today.
> >
> > ( https://www.youtube.com/watch?v=3ZKq2ptu7qw )
> >
> > "In the work of Seldin and others L is defined
> > as FEH, where E is a universal class. Under this
> > definition Hp and L(Kp) are interderivable,
> > but our proof of Proposition 3.10 fails."
> >
> > I wonder where you might note in this paper
> > the relevant type theory analog of set theory's
> > "forcing", applied.
> >
> > I'm looking at definition 2.12 at it looks like
> > the introduction of "infinite union" over
> > regular set theory's usual "pairwise union",
> > and there you go.
> >
> > ( https://www.youtube.com/watch?v=2Abk1jAONjw )

[George Greene]

On Sunday, July 1, 2018 at 3:58:54 PM UTC-4, burs...@gmail.com wrote:
> A<->(A->B), is equivalent to A/\B, in
> classical logic.
>
> A B ((A ↔ (A → B)) ↔ (A ∧ B))
> F F T
> F T T
> T F T
> T T T

...

> Thats another way of proving (A<->(A->B))->B.
> But whats your point?

My point is that NOTHING PARADOXICAL IS GOING ON here!
When (A<->(A->B)) is false, one of A or B must be false as well.
But if A is "If A is true, then B", then you CAN'T MAKE A FALSE AT ALL!
From the assumption that A is false it follows that the quoted conditional
is true, and therefore that A is TRUE,and therefore that B is true.
In the Curry's Paradox case, you get THE SAME A/\B consequent from the
assumption THAT A IS FALSE.

I guess my point is that the assertion of the abbreviation and label
A<->(A->B)
is NOT
A itself.
It is possible for the biconditional to be false while A is true (i.e. if B
is false).

[j4n bur53]

Thats not my paper with |-_red X, thats from
somebody else, Barendregt. I am only the messenger,
don't kill the messenger.

You should really have a look George.

And after you looked at it, you should tell
us how you convert lambda conversion
into your classical conjunction?

One more remark (A/\B->B) could be viewed as:

A,B |- B

holds trivially also in minimal logic, already
from the axiom schema (Id). Which has a simple
typed lambda calculus correspence of typing

a variable:

G, x:A |- x:A

And is also used in the LEM free proof of the
Curry Paradox, see my post from 02.07.18, 20:36,
proof step number #9.

George Greene schrieb:

[burs...@gmail.com]

But we must say Lawrence Paulson does a great
job. He seems to be fully aware of the fine
points of set theory, which Dan Christensen

seems not to be aware. Dan Christensens still
cries like a baby when it comes to classes,
although he even allows quantifying over function

symbols in DC Proof, even if their setlike
status has not be established. So DC Proof is
not strictly FOL. But anyway, the fine points

of set theory as observed by Lawrence Paulson:

6.2 Functional Replacement
Suppose that f is a unary operator on sets —
not a set-theoretic function, which is a set
of pairs, but a meta-level function such as
℘ or U. Since the predicate φ(x, y) ≡ (y = f (x))
is obviously single-valued, define

{f(x).x∈A} ≡ {y.x∈A,y=f(x)}.

This form of Replacement illustrates why
single-valued predicates are sometimes
called class functions. Isabelle can express
meta-level functions by abstraction in
its typed λ-calculus.
https://www.cl.cam.ac.uk/~lp15/papers/Formath/set-I.pdf

So let me reiterate for Dan Christensen, by
already using FOL, there are always unary
operators available which are not setlike

functions, simply by single-value predicates.
we wouldn't even need to go that far as DC Proof
does, and allow quantification over function

symbols. Maybe we could go more primitive, what
metamath allows. Allow class variables, which
can be viewed as represent predicates,

irrespective whether they are single or multi-
valued. But we would need to take care, that
they only get forall quantified in the premisse,

which is not assured for DC Proof. Can I
arbitrarily quantify function symbols? Maybe
I should make a new attempt for some inconsistency

in DC proof from the empty theory, maybe using
some of the predefined extra axioms and
inference rules...

[burs...@gmail.com]

Maybe this is even the right thread for the
search of such an inconsistency, just recall
that Barendregts shows a real problem,

his Curry Paradox is the ultimate explosion:

|-_red X

Just because we allow unrestricted reductions
among lambda terms, we can derive anything
we want. So Lawrence Paulson wrote,

set theory is annoying, since it even allows
self application. That is really what we would
need to recreate the paradox, if one reads

Barendegts paper. In Barendregts paper an
Y = Y -> X is created thanks to self application
reduction. The Y is in fact a more complex lambda

term. So can we recreate the paradox in DC Proof,
or maybe was Lawrence Paulson sloppy, even in
Isabelle/HOL. He says in 6.2 Functional Replacement

that some abstraction is available. This is
either a lie, or it is too powerful and we can
recreate the Curry paradox. Possibly the answer

is more shaded...not yet sure.

[FredJeffries]

How does this earn the label 'rant'? (No, I haven't looked at the source document). What is incorrect in the passage you quote?