my hunch is that we cannot provide any such clear cut distinction — Banno

My hunch is that we can; but my amended attempt might not be satisfactory.

uncountable number of formation rules — Banno

Even just an uncountable set of symbols knocks it out of being formal. For example, in logic, we can have languages with uncountably many symbols (and useful to have for certain purposes, such as in model theory to derive a model upon which to base non-standard analysis), but such a language is not considered formal, since there's no such thing as an uncountable recursive set.

Perhaps one might ask, is that designation arbitrary? — Banno

Yes. It should be.

supose we have the sentences {p, q, r} and designate r as the conclusion. Is that an argument, or is there something more, such that in addition, r is the "logical consequence" of {p.q}? — Banno

No, because that would be defining 'valid argument', not 'argument' in general.

relevant logic — Banno

Don't know how it goes specifically with relevance logic. But my guess is that even in relevance logic, 'argument' would not mean just valid argument.

I take the idea as being as general as possible: The one thing all arguments have in common is having a set of premises and a conclusion. (Sometimes a set of premises and a non-empty set of conclusions*.) Then we find definitions of various notions of validity: whether classical, intuitionistic, relevance, multi-value, etc.

* But I've heard of a notion in which the set of conclusions could be empty.

what is the logical structure of an argument, in contrast to its syntax, grammar, and semantics. — Banno

I don't know what you mean.

The most basic "structure" is that an argument is an ordered pair, with the first coordinate being a set of sentences and the second coordinate being a sentence.

Another way: An argument is a non-empty set of sentences with exactly one of the members designated as the conclusion.

there can't be any sensible doubt that the argument in the OP is valid for formal propositional logic. So in order for those who claim it is invalid to be correct, there must be more than one form of validity, and hence logical pluralism follows. — Banno

That argument doesn't seem for me to work.

A logical monist could say that certain supposed laws of entailment are not correct and thus not laws of logic. It doesn't follow that the monist would be in contradiction if she also said that there are certain laws of entailment that are the only correct laws of logic.

That is, it doesn't seem to me that in denying that certain supposed laws are correct one has to agree that that there are different competing sets of laws that are all correct.

I'm not happy with my response to the question of distinguishing between formal and informal languages.

Your challenge could be taken as: Provide a definition such that any language is exactly one of: formal and informal.

(1) I chose the attribute of having a recursive set of formulas ('formula in the sense of 'well formed formula' in logic). But that I think it should be more general: the set of well formed expressions is a recursive set.

(2) What about formal/informal blends?

(3) Even with ordinary formal languages for logic, there may be other considerations that are required to hold for formality other than that the set of expressions is recursive. (Especially the notion of 'an effectivized language'.)

(4) Other complications.

If P then not P
P
Not P

This is valid and not sound, but also not coherent. — Hanover

It would help if you provided a definition of 'coherent' such that its a matter of form alone.

We do have the definition per form alone of 'inconsistent' (in sentential logic, both equivalent with unsatisfiable, and reducible to per form alone).

The set of premises of the above argument is inconsistent.

/

(0) An argument is valid if and only if there is no interpretation in which all the premises are true and the conclusion is false.

Ways (0) holds:

(1) The set of premises is not satisfiable and the conclusion is logically true.

(2) The set of premises is not satisfiable and the conclusion is contingent.

(3) The set of premises is not satisfiable and the conclusion is logically false.

(4) The set of premises is satisfiable and the conclusion is logically true.

(5) The set of premises is satisfiable and the conclusion is contingent, but there is no assignment in which all the premises are true and the conclusion is false.

(6) Every member of the set of premises is logically true and the conclusion is logically true.

Ways (0) does not hold:

(7) The set of premises is satisfiable and there is an interpretation in which all the premises are true and the conclusion is false.

(8) Every member of the set of premises is logically true and the conclusion is not logically true.

/

We could coin the word 'revonah' (suggesting the opposite of what Hanover likes), and say:

An argument is revonah if and only if its set of premises is not satisfiable.

(1), (2) and (3) are revonah.

If I went to the store, I did not go to the store, and I went to the store, so I did not go to the store." That is valid, but meaningless. I have no idea what you did, whether you went to the store, didn't go to the store, and I can't understand how your going to the store made you not go to the store." — Hanover

Again, valid/invalid in ordinary formal logic pertain to the entailment relation. Indeed, it would be foolish to look for information about the truth of the premises and conclusion merely from consider of validity, except to see that there are no interpretations in which all the premises are true and the conclusion is false.

But, of course, one may hold that the world 'valid' should not be used if it doesn't comport with certain everyday and philosophical senses, though, personally, I understand the notion in ordinary formal logic and allow that words have different special senses in various fields of study.

The incoherently true statement is also distinct from the vacuously true statement. As in, "if Tokyo is in Spain, then the Eiffel Tower is in Bolivia." There the antecedent cannot ever be satisfied — Hanover

The conditional is vacuously true in all interpretations in which 'Tokyo is in Spain' is false. But it is not the case that 'Tokyo is in Spain' is false in all interpretations.

if I've misunderstood this — Hanover

You might understand if you read an introductory textbook in formal logic. You wouldn't have to accept the material, but at least you would see how it operates.

(When I write, 'well formed formula', take that as short for 'well formed formula of the language'.)

Of course, people may have different ideas about what 'formal' means. But at least I think we would find that, for the most part at least, such things that are considered formal languages - such as languages for formal theories, computer languages, etc. - have in common that well formedness and other certain other features are algorithmically checkable.*

If a set is recursive, then there is an algorithm to determine whether something is or is not in that set. So if the set of well formed formulas is recursive, then there is an algorithm to determine whether a given sequence of symbols is or is not a well formed formula.

The desideratum is that it is algorithmically checkable whether a given string is or is not a well formed formula.

And, yes, that is all syntactical.

And the formation rules are chosen so that indeed they provide that the set of well formed formulas of is recursive. So, the rules are given as recursive definitions.

And the inference rules are recursive relations. So the set of proofs is a recursive set. So it is machine checkable whether a sequence of formulas is or is not a proof.

The point is that, with a formal language and formal proof, it is utterly objective whether a sequence of formulas is indeed a proof. A computer or a human following the instructions of an algorithm may (at least in principle) objectively check whether a given purported proof is indeed a proof.

And, yes, all of that is syntactical.

/

* We can also look at notions of 'formal' prior to the advent of recursion theory. And we can look at the general study of modern 'formal languages' that is mostly aimed at formal linguistics and computer science.

You should think of a word for 'follows from' so that it is not conflated with other common senses.

I suggest 'P raps Q' (equivalently, 'Q raps from P') instead of 'Q follows from P'.

('raps' from 'Srap')

I would think 'follows from' is reflexive and transitive, but not symmetric.

I would need to doublecheck these (and depends on knowing more about 'follows from'):

C(P) is consistent if and only if P is not logically false.

If P is contingent, then N(P) is inconsistent.

P is logically false if and only if N(P) = 0. (explosion)

If P is logically true, then N(P) is inconsistent.

Depends on what 'needs' means.

Mathematics pretty much needs sets to work with. But if one denies that mathematics needs to be axiomatized, then mathematics does not need the set theory axioms.

If one affirms that mathematics needs to be axiomatized, then the usual axiomatization is set theory.

I tried to put something together along the lines you have in mind.

The best I came up with is this:

(1) For any sentence P, the set of all sentences is partitioned into two sets: (1) the set of sentences that follow from P, call it C(P) and (2) the set of sentences that do not follow from P, call it N(P). Then instead of sentences, consider sets of sentences, let the negation of C(P) be N(P).

But that's not what you want. So, maybe we would consider the set of sentences not compatible (my word) with P such as "raining" is not compatible with "sunny" (putting aside sun showers). But that uses "not".

So I thought of this:

(2) For any sentence P, the set of the set of all sentences is partitioned into two sets: (1) the set of sentences Q such that {P Q} is satisfiable, call it C*(P) and (2) the set of sentences Q such that {P Q} is not satisfiable, call it N*(P). Then instead of sentences, consider sets of sentences, let the negation of C*(P) be N*(P). But that uses "not".

But then I thought that we should just leave it up to gorillas; and that does seem to work.

specialized sense of consistency ― that P and ~P are inconsistent, for any P — Srap Tasmaner

We have that. You want to use that to define inconsistency in general without using the notions of semantic or syntactical consequence?

you can say A and B are inconsistent if A → C and B → ~C. — Srap Tasmaner

We already have:

If G |- A -> C and G |- B -> ~C, then Gu{A B} is inconsistent.

I don't see what you're bringing.

unless you want to start with the Sheffer stroke — Srap Tasmaner

Or Nicod dagger.

we need both consistency and consequence as core ideas — Srap Tasmaner

Not getting it.

We define consistency from provability. (We could also define it from satisfiability.) Why is that lacking?

any given idea (claim, thought, etc.) has a twin that is the one thing guaranteed under no circumstances to follow from it — Srap Tasmaner

How do you know there is only one thing?

Now it could be that the LNC, so beloved on this forum, functions as a minimal inconsistency guard, and from that you get the rest. — Srap Tasmaner

I don't know what you mean by "minimal inconsistency guard".

Suppose I hold beliefs A and B. And suppose also that A → C, and B → ~C. That's grounds for claiming that A and B are inconsistent, but only because C and ~C are inconsistent. — Srap Tasmaner

Okay.

How would we define the bare inconsistency of C and ~C in terms of consequence? — Srap Tasmaner

What sense of "consequence"? Entailment?

Do you mean how to define 'inconsistent'?

(First order in this post and generally in posts unless said otherwise.)

Or how to show that {C, ~C} is inconsistent? It's trivial. {C ~C} |- C & ~C. But yes, that uses conjunction intro, which is deduction. And since we have {C ~C} |- C & ~C, we have {C ~C} |= C & ~C. (soundness)

Or semantically, it's trivial to show that {C, ~C} is unsatisfiable. And we have that any unsatisfiable set is inconsistent. (completeness)

Or, we could define 'inconsistent' as "proves a formula C and proves ~C". Then, even more trivially, {C ~C} |- C and {C ~C} |- ~C. But even that uses a deduction rule (whatever you call it - inferring a sentence by virtue of it being in the set of premises.) And since we have {C ~C} |- C and {C ~C} |- ~C, we have {C ~C} |= C and {C ~C} |= ~C.


/

Df. a set of sentences is inconsistent if and only if it proves a contradiction.

Th. a set of sentences is inconsistent if and only if it entails a contradiction.

Df. a set of sentences is satisfiable if and only if there is an interpretation in which all the sentences are true.

Th. a set of sentences is inconsistent if and only if it is not satisfiable.

the difference between formal and informal — Banno

We do have a definition of 'formal language': the set of well formed formulas is a recursive set*; and perhaps add unique readability. [EDIT: That might be only a terse synopsis of a definition that might need refinement and other clauses. And I have in mind mainly the kind of languages used in mathematical logic.]

* More exactly, the set of Godel numbers of well formed formulas is a recursive set.

/

Might be interesting to adduce a formal sentence and demonstrate somehow that it can't be said in English alone (not just that all known attempts failed).

For writing, I would accept ordinary punctuation, but don't know about formatting or special characters given an ad hoc role.

Also, I recognize that the burden is not just to show that it would be difficult to use only English but that it would not be possible.

Impressive that you did it without a bot. I just let the bot give me the English translation, but it too used specially formatting - bullet points and indentations.

But don't let the gratuitous complexity distract from the point. We could find examples in actual mathematics that might not be so complex but still tough. And then in the primitive language.

Of course, you can use special formatting to do it, with a convention as to what it signifies. But is that natural? That is, try to do it spoken.

I guess that' similar to the prisoner's dilemma.

So the core idea would be not whether one idea (or claim or whatever) follows from another, but whether two ideas (claims, etc) are consistent with each other. — Srap Tasmaner

Okay, but consistency is defined in terms of derivability (which, in first order, is equivalent with entailment).

Said in natural language? Includes using parentheses to mark arbitrarily deep nested sub-sentences?

In natural language, how would you say?:

∀x ∃y ∀z ((P(x) ∧ ∃u (Q(y) ∨ (R(u) ∧ ∀v (S(v) → T(z, v))))) → ¬(∀w (U(w) ∧ ∃t (V(x, t) → W(t, w))) ∧ ∃p(X(p) ∧ ∀q (Y(q) → Z(p, q)))) ∨ (A(x, y, z) ∧ ∀b ∃c (D(b, c) → (E(x, b, c) ∧ ∃d (F(d) ∧ G(d, x, y)))))

And throw in some math and modal operators too.

∀x ∈ ℝ ∃y ∈ ℝ ∀z ∈ ℕ ((x² + y² = z² ∧ ∃u ∈ ℤ (sin(u) + cos(y) ≥ 1 ∨ (∫₀ᵘ eᵗ dt = eᵘ - 1 ∧ ∀v ∈ ℚ (v > 0 → d/dv (v²) = 2v)))) → ¬(∀w ∈ ℂ (|w| ≤ 1 ∧ ∃t ∈ ℝ⁺ (log(t) ≤ 0 → t ≤ 1)) ∧ ∃p ∈ ℕ (p! = ∏ₖ₌₁ᵖ k ∧ ∀q ∈ ℝ (q ≠ 0 → 1/q ≠ 0))) ∨ (A(x, y, z) ∧ ∀b ∈ ℝ ∃c ∈ ℝ (D(b, c) → (E(x, b, c) ∧ ∃d ∈ ℕ (F(d) ∧ G(d, x, y)))))) ∧ ∀r ∈ ℝ (◻H(r) → ◇I(r))

(I hope that's well formed and displays correctly - it was made by a bot.)

In particular, it's interesting to think of this whole complex of ideas as being "safe" because coherent ― you can jump on the merry-go-around anywhere at all, pick any starting point, and you will find that it works, and whatever you develop from the point where you began will serve, oddly, to secure the place where you started. And this will turn out to be true for multiple approaches to foundations for mathematics and logic. — Srap Tasmaner

Nice.

Interesting. Very much bears looking into.

By the way, I greatly enjoyed the video linked in the 'Logical Nihilism' thread. I have a lot of thoughts about it, and a lot of reading to do about it, but just not the time to put it together as a good post now.

Consistent languages capable of first order arithmetic can't contain their own truth predicate, so we don't put the predicate in. But natural language does contain its own truth predicate and behaves... well it doesn't disintegrate. That's at the very least a type distinction between consistent formal languages and natural language - one can contain its own truth predicate without being crap, one cannot. — fdrake

I'm not sure that I recall Tarski correctly (perhaps he does mention the notion of a 'consistent or inconsistent language'?) But usually languages are not consistent of inconsistent; sets of formulas are consistent or inconsistent. In this part, he's talking about an interpreted formal language. We have that there would be a contradiction (in the meta-theory, whether formal or informal) if such an interpreted formal language had its own truth predicate.

Yes, aside from paraconsistency, we would not comfortably bear contradiction, while we can bear paradox in natural language. But, we need to keep in mind that wide-open natural language doesn't provide the desiderata of formal languages.

Isn't formal language a part of natural language? — Banno

In one view, we have a formal object-language, and an informal or formal meta-language that includes the formal object-language.

Just that there's at least here a dependence of mathematics on natural language, which gives the appearance of being purely pedagogical, or unimportant "set up" steps (still closely related to the thing about logical schemata, from above). — Srap Tasmaner

I don't know of anyone who thinks natural language conveyance of mathematics is unimportant.

the indefinability of "set" — Srap Tasmaner

'set' can be defined from 'element of'.

I imagined Srap and I were talking about how the formalism in mathematics doesn't start at its "grounds", in the axioms. I imagine Srap and I are reacting to an imagined enemy of a formalist who thinks that mathematics is somehow "just" symbol manipulation. Or alternatively just awed at how the root of the formalism is in as something as messy as natural language, despite how set in stone - settable in stone - the concepts of mathematics seem to be. — fdrake

Just to be clear, one form of formalism is the extreme view that mathematics is mere symbol games. But formalism is not at all confined to such an extreme view.

/

Yes, even an extreme game formalist would have to admit that eventually we have to communicate in natural language. (Though he might try the "write the code and send it up in a spaceship to the advanced intelligence creatures" argument.)

And variables are used in both mathematics and everyday discourse. I can see the shape of an argument against the extreme game formalist based on the fact that variables (for example) probably originated naturally. So the argument is this?: Mathematics needs variables, and variables are ultimately understood naturally not formally.

logic as just "given" in toto — Srap Tasmaner

It's more like the chicken and the egg (as you mention later in your post).

You can take the logic as given to base math on it.

And you can take a certain amount of math as given to base logic on it.

Choose your chicken or your egg.

Even formally: You need predicate logic as a basis for Z set theory. And, at least in usual formulations, you need at least some finitistic math to formalize the predicate calculus.

One way of thinking a way out of the bind is to take successive meta-theories, but that would be ad infinitum.

Another way is to point to the coherency: There is credibility as both logic-to-math and math-to-logic are both intuitive and work in reverse nicely.

Another way would be just to display the code for the formal theory without explanation or verification of any aspect of it, and then put in sequences of formulas and see which are ratified as proofs. That is, suppose you uploaded it to a highly intelligent life form, without explanation, and let those creatures discern that it works. Personally, though not necessarily philosophically, that tack doesn't appeal to me.

But, I don't see how to disagree that yes, ultimately, as humans, since we have finite time and can't in a lifetime escalate meta-theories infinitely, ultimately it will boil down to ostensive understanding, just as so much of thinking and use of language seems to do.

member and collection — Srap Tasmaner

Most writers seem to view 'member' and 'set' (or 'class' depending on the treatment) as the base notions. But formally we can do it with just 'member'.

there just is no way around ∈, no way to cobble it together from the other logical constants. — Srap Tasmaner

(1) 'e' is a non-logical constant.

(2) It is not precluded that we may define 'e' from primitives. von Neumann for example.

Just a tendentious turn of phrase, not important. — Srap Tasmaner

'tendentious' is definitely the Word of the Week. The runner-up is 'flows'.

whether we could get away with thinking of its use elsewhere, not only in the sciences, but in philosophy and the humanities, as, in essence, applied mathematics. — Srap Tasmaner

I must misunderstand you? Famously, formal logic is not just studied in philsophy but applied in philosophy.

Don't know what you're driving at. People use variables outside of math books too.

At the outset of talking about unions (U) and intersections (/\), we get an interesting consideration.

For any S, US = {x | there is a y in S such that x in y}

For any non-empty S, /\S = {x | for all y in S, x in y}.

Why non-empty?

U0 no problem. U0 = 0.

But why no /\0? Because:

Roughly put, the subset axiom is: For any set x and describable property P, there is the subset of x whose members are all and only those members of x that have property P.

Now, there is no set of which every set is a member. Why? Because:

Suppose there is a set V such that every set is a member of V. Then there would be the subset of V of all the sets that have the property of not being a member of itself. Then we have Russell's paradox.

So there is no such V.

Now, suppose there is /\0. But every set would be a member of /\0, as seen:

For all y, it is not the case that y in 0. So for all y, if y in 0 then x in y. So every x would be in /\0, so /\0 would be the universal set V, but there is no such set.

Note: I used the word 'because' in the sense of 'since' not causality.

you have to have sets (or an equivalent) to do much of anything in the rest of mathematics, but so what? — Srap Tasmaner

Set theory axiomatizes classical mathematics. And the language of set theory is used for much of non-classical mathematics. Those are two answers to "so what?"

What does mathematics get out of pretending it's importing logic from elsewhere? — Srap Tasmaner

What pretending? Would you mention a specific writing?

I think of mathematical logic sub-subject of formal logic.

I guess because logic and formal logic have under philosophy, and mathematical is a part of formal logic, we have mathematical logic under the wide umbrella too.

Mathematical logic is typically a course in Mathematics. But sometimes such things as set theory are taught as a Philosophy course.

Symbolic logic is often found as a Philosophy course. But it can be a warmup for mathematical logic, and it usually includes translation of natural language arguments; even if one goes on to use symbolic logic mainly for mathematics, it helps to first know how to translate natural language since so much of mathematical prose is in natural language.

And, of course, mathematical logic is extended in formal logics regarding all kinds of philosophical subjects - modal, epistemic, etc. And, of course, in philosophy of language. And, prominently, computing.

And, of course, philosophy of mathematics is steeped in considerations about mathematical logic, set theory and mathematics.

motivates category theory — Srap Tasmaner

Category theory centers on arrows, and as involving functions, composition of functions and morphisms and things.

Unforgiving when authors were too slapdash or handwavy about this, which I thought showed good philosophical sense. — Srap Tasmaner

Yet, often censoriously regarded as bad philosophical sense in The Philosophy Forum.

are you sure this is right? — Srap Tasmaner

Absolutely sure.

If x in 0 then x in 0.

That's an instance of P -> P.

do we want to say it's because of the proof that it is so? — Srap Tasmaner

I don't opine as to 'because'.

"holds by" ― rather than, "is proved using" — Srap Tasmaner

I meant 'is proved by'. I find that the word 'holds' is used in at least two senses in mathematics: (1) is true, (2) is proven. But with set theory, 'true' could be taken as 'true in any model of the set theory axioms'. So "0 subset of 0" is proven by deploying "P -> P" and it is also true by deploying "P -> P" (given the soundness theorem in this version: if a sentence is provable from a set of axioms then the sentence is true in any model of the axioms).

Another friendly picking of nits: Some writers use the word 'contained'; it is not wrong. But sometimes I see people being not clear whether it means 'member' or 'subset', so I don't use the word. I just say 'member of' or 'subset of' as suited.

One other tiny point of unity: I always thought it was interesting that for "and" and "or" probability just directly borrows ∩ and ∪ from set theory. These are all the same algebra, in a sense, logic, set theory, probability. — Srap Tasmaner

The duals run all through logic and mathematics. The main result concerning propositional logic is that there is an isomorphism between propositional logic and the Tarski-Lindenbaum algebra (a particular Boolean algebra). Then Tarski also showed an isomorphism between predicate logic and cylindrical algebra (the details of cylindrical algebra are beyond mere)

replace set theory entirely — Srap Tasmaner

I'm not expert either. But my understanding is that yes, category theory couches mathematics in different terms from set theory, and thus provides a different way of thinking, but category theory is inter-interpretable with ZFC+"exists an inaccessible cardinal"*. And ZFC+"exists an inaccessible cardinal" provides a model of ZFC, so it is a quite strong theory in that sense.

* But I have never been able to find what that really means. I know what interpretability is. And I know what ZFC+"exists and inaccessible cardinal" is. But interpretability is between two theories, but what exactly is the theory category theory that is inter-interpretable with ZFC+"exists and inaccessible cardinal"?

/

Peter Smith offers some nice content. And he used to post at sci.logic, but, if I recall correctly, got disgusted with all the cranks.

0 subset of 0 holds by P -> P.

Then let me nitpick that. You didn't mean 'nitpick' pejoratively, but subset vs member is not a nitpick, and the point about circularity is a good catch.

Your probability exploration is interesting. I think there's probably (pun intended) been a lot of work on it that you could find.

Indeed, logic and mathematics - chicken and the egg.

I am not up to speed on category theory though I know some of its basics. One problem I've had is finding an axiomatization. However, ZFC+"exists an infinite cardinal" is an axiomatization of category. So, as far as I can tell, category theory does not eschew set theory but rather, and least to the extent of interpretability (different sense of 'interpretation' in this thread) it presupposes it and goes even further.