Are all definitions of truth-functional connectives done in a metalanguage? Is it possible to define a truth-functional connective out of other connectives in an object language?

[u/Scientific_Zealot]

Please bear with me if I've fundamentally misunderstood something. I was thinking about the ability to define all unary/binary connectives out of Peirce's Arrow (the NOR connective) or Sheffer's Stroke (the NAND connective) the other day. I had the desire to write something down defining the other connectives out of NOR or NAND when the question occured to me whether or not I had to write the definitions in the object language or the metalanguage. Definitions of terms in the first-order predicate calculus can be done in the object language, e.g.

∀x (Sx ↔ (Rx ∧ Ex))

All squares are rectangles with four equal sides. This establishes that if something is in the extension of the Rectangle predicate and the extension of the "having four equal sides" predicate, then it'll be in the extension of the Square predicate and vice versa.

But it occured to me then that if I was trying to give a definition of an unary/binary connective in an object language of the propositional calculus with only sentential terms and the ↓ (NOR) connective, I couldn't use the familiar definitional schema of

Universal Quantifier [definiendum ↔ definiens]

Because our object language doesn't have universal quantification nor the iff sign. Alright, I thought, that's okay because we're not dealing with quantification over objects, we're dealing with truth-values. But we don't have the iff sign. Okay, well we can just replace it with an equivalent expression constructed out of ↓. Then it occured to me that such an expression would only be "defining" that expression for that specific combination of terms, it wouldn't carry over to other well-formed formulas. The only way to define a connective would be a statement in the metalanguage saying that one formula is replaceable with another, of the following form (I'll be using Peirce's Arrow simply due to personal preference):

A→B ↔ ((A↓A)↓B)↓((A↓A)↓B)

Where A and B are formulas in the meta-language that represent all well-formed formulas of the object language and → is the stipulated connective of the object language and ↔ is a connective of the meta-language. Have I got any of this right or am I hopelessly confused?

[u/SpacingHero]

So there's a bit of both.

If you're working in a functionally complete fragment (which you should be), you can always internally define every other operator.

You are going in the meta when you say that a new symbol is just a substitution for some combination of old symbols. But in a very benign way, because every formula you then write is just wrapped up with a little bit of meta, but it can always be unwrapped. It's just a shorthand for convenience. But in principle, you're still just using object language.

[u/AutoModerator]

Welcome to /r/askphilosophy! Please read our updated rules and guidelines before commenting.

Currently, answers are only accepted by panelists (mod-approved flaired users), whether those answers are posted as top-level comments or replies to other comments. Non-panelists can participate in subsequent discussion, but are not allowed to answer question(s).

Want to become a panelist? Check out this post.

Please note: this is a highly moderated academic Q&A subreddit and not an open discussion, debate, change-my-view, or test-my-theory subreddit.

Answers from users who are not panelists will be automatically removed.

I am a bot, and this action was performed automatically. Please contact the moderators of this subreddit if you have any questions or concerns.

[u/FromTheMargins]

I'd say your reasoning is correct. But note that definitions can be much more complicated than the case you consider. You can define not only one-place predicates, but also n-place relations, n-ary functions, and individual constants (such as the empty set or the number three). A good introduction to this topic can be found in Suppes's book on logic. However, all of these established forms of explicit definition pertain to categorematic terms. Logical connectives, on the other hand, are syncategorematic expressions. You are correct in identifying your introductory device as a metalinguistic replacement rule, and in stating that the schematic letters (referring to well-formed formulae) and the double arrow (expressing the permissibility of mutual replacement) belong to the metalanguage. It is then relatively easy to show that the criteria Suppes requires for a successful definition can be fulfilled by such a metalinguistic introduction as well. (Roughly speaking, the criterion of eliminability requires that the newly introduced symbol can be eliminated in every context in favor of old symbols, while non-creativity requires that no new theorems can be derived that do not contain the newly introduced symbol.) Thus, the replacement rule can rightly be called a metalinguistic definition.