If I'm not mistaken, Von Neumann formalized without 'element' as primitive in 1925.
— TonesInDeepFreeze

Would be most interested in a reference or more context. — fishfry

The original paper is in Jean van Heijenoorts's 'From Frege To Godel'.

I don't know, because I got confused by what different people said at StackExchange.

Those are my questions to sort out the discussion at StackExchange. You can post it if you want, but I probably won't follow up there or here, as I explained.

It's certainly interesting that one can do set theory without elements. — fishfry

If I'm not mistaken, Von Neumann formalized without 'element' as primitive in 1925.

First, for your questions, these still need to be clearly settled:

(1) Given a recursively axiomatizable theory with finitely many axioms, and with 'length of proof' defined as the sum of the lengths of the formulas that are the lines in the proof, is there an algorithm to determine. for any given theorem, the least length of a proof?

(2) Given a recursively axiomatizable theory with infinitely many axioms, and with 'length of proof' defined as the sum of the lengths of the formulas that are the lines in the proof, is there an algorithm to determine, for any given theorem, the least length of a proof?

(3) Given a recursively axiomatizable theory with finitely many axioms, and with 'length of proof' defined as the number of lines in the proof, is there an algorithm to determine, for any given theorem, the least length of a proof?

(4) Given a recursively axiomatizable theory with infinitely many axioms, and with 'length of proof' defined as the number of lines in the proof, is there an algorithm to determine, for any given theorem, the least length of a proof?

At least for now, I've decided not to post there. There are already too many confusions in the discussions, and I'm not up to sorting through them with the participants. Also, I don't like the interface and layout of the post and thread formatting there.

a recursive set is not the same thing as a recursively enumerable set, — tim wood

In the exact sense that the set of recursive sets is a proper subset of the set of recursively enumerable sets.

closure — tim wood

A theory is closed under deduction.

But the clause you have in mind is recursive axiomatizability. (I don't think that is usually referred to as 'closure'.)

Mathematics Made Difficult by Linderholm — jgill

I looked at the description of that book. It's a fun and clever idea.

What does that have to do with the relationship between mathematical logic and set theory?

The very first sentence in the very first reply to you in that thread:

"What does it mean for a theorem to be complete or uncountable?"

Please stop using the phrases "theorem is complete" or "theorem is countable". They make no sense, and all they do is make people have to stop you in your tracks before we can even answer you about anything else you ask or say.

What do you think — Shawn

I would have to think it through. I am simply not caught up in the StackExchange thread.

recursively enumerable is not the same as recursive, and implies non-recursiveness. — tim wood

That is incorrect.

It is an easy theorem that R is recursive iff (R is recursively enumerable & ~ R is recursively enumerable).

A recursive enumeration does not itself provide a decision procedure for R, but that does not entail that there does not exist a decision procedure for R.

an axiom I understand here is an expression, like Godel's sentence, such that neither it nor its negation is provable, yet is also provably true, being proved meta-mathematically — tim wood

That is incorrect. You have conflated "formula F is independent of axiom set S" with "formula F is an axiom in the axiom set S".

Axiomatization is a relation between a set of sentences (called 'the axioms') and the set of sentences (called 'the theorems') that are provable from those axioms. I.e.:

A set of sentence S is an axiomatization of a set of sentences T iff every member of T is provable from some finite subset of S.

A theory is a set of sentence closed under deduction (provability).

A recursive axiomatization S of a theory T is a recursive set of sentences S such that every member of T is provable from a finite subset of S.

Trivially, any axiom in S is provable from S. (Trivially, any axiom is provable from itself.)

A theory T is recursively axiomatizable iff there is a recursive set S that is an axiomatization of T.

/

Here, 'computable' is to be taken as 'Turing machine computable'.

"If R is recursive then R is Turing machine computable".

That has a long and complicated proof, but it's not controversial that it is proven.

Note that this does not even need to assume the Church-Turning thesis, as its converse ("If R is recursive then R is computable (in an intuitive informal sense of 'computable')") is not controversial.

That's a very modest claim.

That there is a recursive axiomatization of a theory T entails that it is computable whether any given string is or is not an axiom.That follows from the fact that any recursive relation is computable.

By the way, I don't know what would be the value in telling others that I said it, since I am not in any way an authoritative expert in logic of mathematics. The only thing I really know very much about is jazz.

I am interested to see what people there say about your notion of a 'complete theorem'.

I asked you previously: Do you understand the difference between a theory and a theorem?

It's too much work for me to try to have you make that quote understandable.

If the language is uncountable, then the theory is not recursively axiomatizable and is not a formal theory. And, yes, Godel's theorem pertains only to formal theories.

A book you should read:

Godel's Theorem: An Incomplete Guide To Its Use and Abuse - Franzen.

It's not a technical tome, and I bet it would answer a lot of your questions right away.

how do you discern axioms in the theorem that are non-computable from those that are computable. — Shawn

What do you mean by 'computable axiom'?

'recursive axiomatization' is given a rigorous definition. With a theory that is recursively axiomatizable, it is computable whether a symbol string is or is not an axiom. And we may stipulate that we are using effectivized languages. In ordinary cases, if the theory is recursively axiomatizable, then we know an algorithm for checking whether a symbol string is or is not an axiom.

As Wiles said when he proved Fermat's last theorem at a conference: "I think I'll stop now." — fishfry

As Miles Davis said to producer Alfred Lion, "Is that what you wanted, Alfred?"

Or, just after Davis, Hancock, Carter and Williams laid down "Thisness" - an exceptionally gorgeous, introspective, haunting modern and abstract ballad - producer Teo Macero said to the group, "Your sandwiches are here."

I don't think TonesInDeepFreeze quite has that attitude though — Metaphysician Undercover

Mote and Beam!

In an earlier post, when I was editing, somehow I cut a part that is helpful about the axiom schema of separation. I added it back:

That says: If you have a set z, then you can form the subset x of z such that the members of x are all and only those members of z that have property P.

In other words, In other words, instead of using a property to define a set in an unrestricted manner, you do it by using that property to make a subset of an already given set.

With P being ~yey, with the axiom schema of separation, we have:

AzExAy(yex <-> (yez & ~yey)).

And that doesn't yield a contradiction. — TonesInDeepFreeze

(1) Start by learning basic symbolic logic, which is the first order predicate calculus. The best textbook I have found is:

'Logic: Techniques Of Formal Reasoning' - Kalish, Montague and Mar

Supplement that with the best chapter I have found on the subject of mathematical definitions:

chapter 8 in 'Introduction To Logic; - Suppes

(2) Then basic axiomatic set theory. The book I like best is:

'Elements Of Set Theory' - Enderton

Supplement, if you like with:

'Axiomatic Set Theory' - Suppes

(3) Then basic mathematical logic. The book I like best is:

'A Mathematical Introduction To Logic' - Enderton

(4) The above book takes you through a proof of Godel's incompleteness theorem. After that, a more relaxing but wonderfully insightful read is a brilliant and beautifully written book for the layman on incompleteness:

'Godel's Theorem: An Incomplete Guide To It Use And Abuse' - Franzen

(4) At any point during this study, you can read what I have found to be the best general overview of the background for logic. That is:

the Introduction chapter in 'Introduction To Mathematical Logic' - Church

(5) If you like, you can put your toes in the water of other kinds of logic. An excellent overview is:

'An Introduction To Non-Classical Logic' - Priest

/

All of those books are widely used and considered to be authoritative. They will give you vocabulary and concepts that are common in discourse on logic and set theory.

This course of reading would arm you with a solid understanding that provides a foundation for more studies, if you like, at a graduate level that includes a panoply of rich and fascinating investigations.

Given clarity in discussion about it, yes, it is interesting. It's something I have wondered about before.

If I have time later, maybe I'll reply on StackExchange to better understand some of the points.

For me, mathematical logic and set theory are chicken and egg. To formalize set theory, we use the first order predicate calculus, which is a subject of mathematical logic. But to formalize mathematical logic, we use set theory. So I don't think we should put one below the other in a tree.

(And I don't know why Algebra is placed between them on that tree. Granted, propositional logic can be described as a Boolean algebra, and first order logic as a cylindric algebra, but those results themselves can be described set theoretically.)

I read that.

I was going to write:

"I should have stipulated that we're talking about finitely axiomatizable theories. Even if the theory is recursively axiomatizable but not finitely axiomatizable, then the method would not work."

So I thought his argument was correct. But then I saw that he amended to say that brute method would work if 'length' is defined by symbols not lines. (And we did define by symbols not lines.) So, by his amended argument, the paragraph above in which I correct myself is not correct and I never needed to correct myself except to include that the theory is recursively axiomatizable. But I don't see why his original argument is still not correct, whether it's symbols or lines. So I am confused.

I would title it:

Problem of finding shortest proof - how complex is it?

But I really have to warn that, since I'm not really informed on this particular subject, my own formulation might get shot down.

Darn. I need to edit my reply.

Can you edit your stackexchange post?

(I think complexity class pertains to the problem not the algorithm?)

This is better:

For first order theories, is it correct that there is a brute force algorithm that tells us the shortest proof length for any given theorem ('length' means the sum of the lengths of the formulas that appear as lines in the proof)? Are there algorithms better than brute force? What is the complexity class for the problem?

how does the machine do this without a brute force method? — Shawn

I'm still not sure what your question is. Also, I'm not very informed about complexity, so my own formulation might need correction too. But here's my best try:

For first order theories, is it correct that there is a brute force algorithm that tells us the shortest proof length for any given theorem ('length' means the sum of the lengths of the formulas that appear as lines in the proof)? What is the complexity class for the algorithm? Are there algorithms better than brute force? What is the least complexity class for an algorithm to tell us the shortest proof length?

how does the machine do this without a brute force method? — Shawn

The method I mentioned is brute force. I don't know whether there's a better method.

A machine for ascertaining the length of the shortest proof of a theorem doesn't involve anything like oracles.

If I'm not mistaken, this is not about unsolvable problems. Rather, it's about finding out the complexity of the algorithm for deciding this decidable problem.

I surmise that he's not asking about degree of unsolvability but about the complexity of the problem.

4.1 Significance of Complexity here: https://plato.stanford.edu/entries/computability/

class complexity — Shawn

Not 'class complexity'. The 'complexity class'.

No, I addressed exactly the sentence he wrote. What he wrote in that sentence was correct. I am not responsible for addressing other confusions he has that might conflict with the sentence he posted and to which I responded. He wrote something correct, and I affirmed it.

He said that he thinks PM solves the problem with types but that he might have to look it up to be sure.

I said he doesn't have to look it; he is correct that PM avoids the paradox.

You seem to be confused.

It is correct that PM is one approach to avoiding the paradox. With PM there is no set of all sets.

I do not believe there is a set of all sets either in Russell's type theory or in any version of modern type theory. I'd be grateful if you could supply references and/or context to the contrary. — fishfry

Why would I want to supply references to a claim that PM allows a set of all sets when I agree that PM does not allow a set of all sets?

You don't need to search. You are correct that PM is one approach to avoiding the paradox.

How do you make it both syntactic and semantical within a formal system to ascertain the Turing complexity of the task — Shawn

I have no idea what you mean.

What does "this" refer to there? Set theory can't do a lot of things, but what is it in particular are you saying set theory can't do?
— TonesInDeepFreeze

Sorry, I was thinking about it dialectically with regards to type theory, which I explained my thoughts about above in the post above. — Shawn

I have no idea what you mean.

Are you deliberately wasting people's time with remarks you've intentionally prepared to be gibberish or are so personally esoteric that no one but you could know what you mean?