Do definitions have to fit axioms in logic?

Clash Royale CLAN TAG#URR8PPP

up vote
5
down vote

favorite

1

One thing I find confusing in propositional logic is that we have things like axioms and inference rules but then we seem to be able to define whatever we want in syntax that doesn't necessarily adhere to the axiom formats.

For example

https://en.wikipedia.org/wiki/Propositional_calculus#Example_1._Simple_axiom_system

This example system uses the modus ponens inference rule:

$P, P to Q vdash Q$

And the following axioms:

I. $(p to (q to p))$

II. $((p to (q to r)) to ((p to q) to (p to r)))$

III. $((lnot p to lnot q) to (q to p))$

We have the $lnot$ and $to$ operator in the language but then we define $a land b = lnot(a to lnot b)$ even though this format does not match any of the three axioms, nor have we defined equality.

Why is this permitted? What are we allowed to define? What are we even using modus ponens and the axioms for if we can just make up whatever?

logic definition propositional-calculus axioms metalogic

share|cite|improve this question

edited Sep 4 at 23:41

asked Sep 4 at 23:34

user525966

1,537619

• 
  
  
  

  
  

  
  
  
  
  
  

  
  see van Dalen, page 30 : "As usual “$¬Ï•$” is used here as an abbreviation for “$ϕ →⊥$”. It is a convention adopted in the metalogic context.
  – Mauro ALLEGRANZA
  Sep 5 at 6:19
  

  
  
  
  


• 
  
  
  

  
  

  
  
  
  
  
  

  
  For formal definitions "inside" the calculus (FOL) see the post : Semantics and Logical structure in Definitions as well as the post Theory of definitions.
  – Mauro ALLEGRANZA
  Sep 5 at 6:57
  
  

  
  
  
  


• 
  
  
  

  
  

  
  
  
  
  
  

  
  @MauroALLEGRANZA: Many logic texts do not adopt that convention that you mentioned. Doing so is advantageous for treating intuitionistic logic, but from a classical logic viewpoint I find such an abbreviation to be unnatural.
  – user21820
  Sep 5 at 12:04
  

  
  
  
  


• 
  
  
  

  
  

  
  
  
  
  
  

  
  @user525966: By the way, feel free to come to the Logic chat-room for further inquiry. =)
  – user21820
  Sep 5 at 12:05
  

  
  
  
  

add a comment | 

up vote
5
down vote

favorite

1

One thing I find confusing in propositional logic is that we have things like axioms and inference rules but then we seem to be able to define whatever we want in syntax that doesn't necessarily adhere to the axiom formats.

For example

https://en.wikipedia.org/wiki/Propositional_calculus#Example_1._Simple_axiom_system

This example system uses the modus ponens inference rule:

$P, P to Q vdash Q$

And the following axioms:

I. $(p to (q to p))$

II. $((p to (q to r)) to ((p to q) to (p to r)))$

III. $((lnot p to lnot q) to (q to p))$

We have the $lnot$ and $to$ operator in the language but then we define $a land b = lnot(a to lnot b)$ even though this format does not match any of the three axioms, nor have we defined equality.

Why is this permitted? What are we allowed to define? What are we even using modus ponens and the axioms for if we can just make up whatever?

logic definition propositional-calculus axioms metalogic

share|cite|improve this question

edited Sep 4 at 23:41

asked Sep 4 at 23:34

user525966

1,537619

• 
  
  
  

  
  

  
  
  
  
  
  

  
  see van Dalen, page 30 : "As usual “$¬Ï•$” is used here as an abbreviation for “$ϕ →⊥$”. It is a convention adopted in the metalogic context.
  – Mauro ALLEGRANZA
  Sep 5 at 6:19
  

  
  
  
  


• 
  
  
  

  
  

  
  
  
  
  
  

  
  For formal definitions "inside" the calculus (FOL) see the post : Semantics and Logical structure in Definitions as well as the post Theory of definitions.
  – Mauro ALLEGRANZA
  Sep 5 at 6:57
  
  

  
  
  
  


• 
  
  
  

  
  

  
  
  
  
  
  

  
  @MauroALLEGRANZA: Many logic texts do not adopt that convention that you mentioned. Doing so is advantageous for treating intuitionistic logic, but from a classical logic viewpoint I find such an abbreviation to be unnatural.
  – user21820
  Sep 5 at 12:04
  

  
  
  
  


• 
  
  
  

  
  

  
  
  
  
  
  

  
  @user525966: By the way, feel free to come to the Logic chat-room for further inquiry. =)
  – user21820
  Sep 5 at 12:05
  

  
  
  
  

add a comment | 

up vote
5
down vote

favorite

1

up vote
5
down vote

favorite

1

1

One thing I find confusing in propositional logic is that we have things like axioms and inference rules but then we seem to be able to define whatever we want in syntax that doesn't necessarily adhere to the axiom formats.

For example

https://en.wikipedia.org/wiki/Propositional_calculus#Example_1._Simple_axiom_system

This example system uses the modus ponens inference rule:

$P, P to Q vdash Q$

And the following axioms:

I. $(p to (q to p))$

II. $((p to (q to r)) to ((p to q) to (p to r)))$

III. $((lnot p to lnot q) to (q to p))$

We have the $lnot$ and $to$ operator in the language but then we define $a land b = lnot(a to lnot b)$ even though this format does not match any of the three axioms, nor have we defined equality.

Why is this permitted? What are we allowed to define? What are we even using modus ponens and the axioms for if we can just make up whatever?

logic definition propositional-calculus axioms metalogic

share|cite|improve this question

edited Sep 4 at 23:41

asked Sep 4 at 23:34

user525966

1,537619

One thing I find confusing in propositional logic is that we have things like axioms and inference rules but then we seem to be able to define whatever we want in syntax that doesn't necessarily adhere to the axiom formats.

For example

https://en.wikipedia.org/wiki/Propositional_calculus#Example_1._Simple_axiom_system

This example system uses the modus ponens inference rule:

$P, P to Q vdash Q$

And the following axioms:

I. $(p to (q to p))$

II. $((p to (q to r)) to ((p to q) to (p to r)))$

III. $((lnot p to lnot q) to (q to p))$

We have the $lnot$ and $to$ operator in the language but then we define $a land b = lnot(a to lnot b)$ even though this format does not match any of the three axioms, nor have we defined equality.

Why is this permitted? What are we allowed to define? What are we even using modus ponens and the axioms for if we can just make up whatever?

logic definition propositional-calculus axioms metalogic

share|cite|improve this question

edited Sep 4 at 23:41

asked Sep 4 at 23:34

user525966

1,537619

share|cite|improve this question

share|cite|improve this question

edited Sep 4 at 23:41

edited Sep 4 at 23:41

edited Sep 4 at 23:41

asked Sep 4 at 23:34

user525966

1,537619

asked Sep 4 at 23:34

user525966

1,537619

asked Sep 4 at 23:34

user525966

1,537619

1,537619

• 
  
  
  

  
  

  
  
  
  
  
  

  
  see van Dalen, page 30 : "As usual “$¬Ï•$” is used here as an abbreviation for “$ϕ →⊥$”. It is a convention adopted in the metalogic context.
  – Mauro ALLEGRANZA
  Sep 5 at 6:19
  

  
  
  
  


• 
  
  
  

  
  

  
  
  
  
  
  

  
  For formal definitions "inside" the calculus (FOL) see the post : Semantics and Logical structure in Definitions as well as the post Theory of definitions.
  – Mauro ALLEGRANZA
  Sep 5 at 6:57
  
  

  
  
  
  


• 
  
  
  

  
  

  
  
  
  
  
  

  
  @MauroALLEGRANZA: Many logic texts do not adopt that convention that you mentioned. Doing so is advantageous for treating intuitionistic logic, but from a classical logic viewpoint I find such an abbreviation to be unnatural.
  – user21820
  Sep 5 at 12:04
  

  
  
  
  


• 
  
  
  

  
  

  
  
  
  
  
  

  
  @user525966: By the way, feel free to come to the Logic chat-room for further inquiry. =)
  – user21820
  Sep 5 at 12:05
  

  
  
  
  

add a comment | 

• 
  
  
  

  
  

  
  
  
  
  
  

  
  see van Dalen, page 30 : "As usual “$¬Ï•$” is used here as an abbreviation for “$ϕ →⊥$”. It is a convention adopted in the metalogic context.
  – Mauro ALLEGRANZA
  Sep 5 at 6:19
  

  
  
  
  


• 
  
  
  

  
  

  
  
  
  
  
  

  
  For formal definitions "inside" the calculus (FOL) see the post : Semantics and Logical structure in Definitions as well as the post Theory of definitions.
  – Mauro ALLEGRANZA
  Sep 5 at 6:57
  
  

  
  
  
  


• 
  
  
  

  
  

  
  
  
  
  
  

  
  @MauroALLEGRANZA: Many logic texts do not adopt that convention that you mentioned. Doing so is advantageous for treating intuitionistic logic, but from a classical logic viewpoint I find such an abbreviation to be unnatural.
  – user21820
  Sep 5 at 12:04
  

  
  
  
  


• 
  
  
  

  
  

  
  
  
  
  
  

  
  @user525966: By the way, feel free to come to the Logic chat-room for further inquiry. =)
  – user21820
  Sep 5 at 12:05
  

  
  
  
  

see van Dalen, page 30 : "As usual “$¬Ï•$” is used here as an abbreviation for “$ϕ →⊥$”. It is a convention adopted in the metalogic context.
– Mauro ALLEGRANZA
Sep 5 at 6:19

see van Dalen, page 30 : "As usual “$¬Ï•$” is used here as an abbreviation for “$ϕ →⊥$”. It is a convention adopted in the metalogic context.
– Mauro ALLEGRANZA
Sep 5 at 6:19

For formal definitions "inside" the calculus (FOL) see the post : Semantics and Logical structure in Definitions as well as the post Theory of definitions.
– Mauro ALLEGRANZA
Sep 5 at 6:57

For formal definitions "inside" the calculus (FOL) see the post : Semantics and Logical structure in Definitions as well as the post Theory of definitions.
– Mauro ALLEGRANZA
Sep 5 at 6:57

@MauroALLEGRANZA: Many logic texts do not adopt that convention that you mentioned. Doing so is advantageous for treating intuitionistic logic, but from a classical logic viewpoint I find such an abbreviation to be unnatural.
– user21820
Sep 5 at 12:04

@MauroALLEGRANZA: Many logic texts do not adopt that convention that you mentioned. Doing so is advantageous for treating intuitionistic logic, but from a classical logic viewpoint I find such an abbreviation to be unnatural.
– user21820
Sep 5 at 12:04

@user525966: By the way, feel free to come to the Logic chat-room for further inquiry. =)
– user21820
Sep 5 at 12:05

@user525966: By the way, feel free to come to the Logic chat-room for further inquiry. =)
– user21820
Sep 5 at 12:05

add a comment | 

4 Answers
4

active

oldest

votes

up vote
4
down vote



accepted

Your question arises from the failure of many texts in properly distinguishing between the meta-system and the actual formal system under study. You, at all times, are doing mathematics in the meta-system, and in the field of mathematical logic you are studying some formal system (such as the one you have here with some syntactic rules for forming well-formed formulae (wff) and one deductive rule and three axioms). So, let us precisely express them, and you will see.
$
defquote#1``#1"
defmeta#1mathbindot#1
$

Syntactic rules

Note that wffs are strings. Given any two strings $x,y$ we shall use "$x+y$" to denote the concatenation of $x$ followed by $y$. We shall also use quotes to specify literal strings. For example, you are a person but "you" is a string.

Closure under negation: Given any wff $A$, the string $quoteneg+A$ is also a wff.

Closure under implication: Given any wffs $A,B$, the string $quote(+A+quoteto+B+quote)$ is also a wff.

Note how I used quote-marks above. It would be technically incorrect to write:

... the string $(A to B)$ is also a wff. (technically incorrect)

Because the "$to$" and the brackets are symbols in the formal system under study, not symbols in the meta-system we are using!

Deductive rules

The system under study has only one deductive rule:

Given any wffs P,Q, if you have deduced $P$ and $quote(+P+quoteto+Q+quote)$, then you can deduce $Q$.

Again, note how I used quote-marks.

Abbreviative definitions

Now we come to the so-called 'definition' of "$land$":

Take any strings $A,B$. The string $quote(+A+quoteland+B+quote)$ is not a wff in the formal system under study, simply because "$land$" is not a symbol in its language. However, we wish to use that string to stand for $quoteneg(+A+quotetoneg+B+quote)$.

This wish is not trivial to fulfill rigorously. The easiest way to do it correctly is to add a syntactic rule for closure of wffs under $quoteland$:

Closure under conjunction: Given any wffs $A,B$, the string $quote(+A+quoteland+B+quote)$ is also a wff.

and then check that you can still uniquely parse (interpret) a wff, so that it makes sense to stipulate that $quote(+A+quoteland+B+quote)$ is rewritten as $quoteneg(+A+quotetoneg+B+quote)$ before parsing, to obtain our wish.

As you observed, such a rewrite-rule is not an axiom.

What is that 'equality'?

Note that I did not say that $quote(+A+quoteland+B+quote)$ is the same string as $quoteneg(+A+quotetoneg+B+quote)$, because it is of course false. We are only using a rewrite-rule; the strings themselves are not equal.

You are equally free to 'define' any other notation in the same fashion, using rewrite-rules, and you would have to deal with the same issue of unique parsing. This happens in mathematics itself as well. When you define a new notation it is important that there is still only one way to read things.

So while it is technically wrong to state this rewrite-rule as an equality, it is intuitively 'equal' in the sense of being logically equivalent, since the final parsing is the same.

---

I hope that this addresses your inquiry. If everything is clear, you can continue reading. There is a different way to go about logic that would actually make what is technically wrong above correct, but it may be confusing unless you fully understand the more concrete way above.

Meta-operators

First let us see how we can abstract out the wff formation:

Given any string $A$, define $metaneg A = quoteneg+A$.

Given any strings $A,B$, define $A metato B = quote(+A+quoteto+B+quote)$.

Note that unlike the strings $quoteneg$ and $quoteto$, $metaneg$ and $metato$ are operations on strings (in the meta-system). So we can in fact do the following:

Given any strings $A,B$, define $A metaland B = metaneg( A metato (metaneg B) )$.

Note that the brackets here are in the meta-system, used so that we know which string operation to perform first. If we use the typical precedence rules, namely that $metaneg$ is higher precedence than $metato$, then we could have done the following:

Given any strings $A,B$, define $A metaland B = metaneg( A metato metaneg B )$.

A more abstract way to conceptualize this is that $metato$ and $metaneg$ are actually operations on parse trees rather than strings, and so the above definition of $metaland$ is just a definition of a new operation on parse trees in terms of previously defined ones.

The question that may arise at this point is: Why don't we do it this way and not use strings at all? The simple answer is that the only way to completely formalize a formal system is to be able to encode it into some linear representation such as strings, so you are still going to have to decide on how exactly to encode wffs as strings. Similarly when you use logic on paper. Hence the concrete first approach is ultimately the practical way.

share|cite|improve this answer

answered Sep 5 at 4:52

user21820

36.2k440140

add a comment | 

up vote
8
down vote

You can define anything you want. However, the point of defining something is to make it easier to refer to, which means that the most useful definitions are for things that are:

(a) frequently referred to;

(b) not trivial; and often

(c) similar to something else

So, for example, we define $wedge$ because it allows for a lot of shortcuts in writing the propositional logic, and it happens to align with the general understanding of the word "and". The "=" in the definition isn't really part of the logic, it's a part of the language surrounding it, and we know that there's a level at which we have to resort to shared understanding since you can only abstract things so far.

On the other hand, I probably wouldn't bother coming up with a definition for "the set of all even prime numbers in $mathbbN$", because it's simple enough to just say $2$. Or if I did define it, it would only be for a very limited context (for example, one where I actually needed to prove that 2 is the only element in the set), so I could get away with a generic definition like $A$.

share|cite|improve this answer

answered Sep 4 at 23:43

ConMan

7,1861324

• 
  
  
  

  
  5
  

  
  
  
  
  
  

  
  @user525966 - The only thing that hasn't been mentioned, because I believe it was presumed clear, is that such definitions are just informal abbreviations. I hope it doesn't need explanation that using a shorthand for an expression doesn't require us to know about, and doesn't change anything about, whether that expression is true or not.
  – Malice Vidrine
  Sep 5 at 0:38
  

  
  
  
  


• 
  
  
  

  
  2
  

  
  
  
  
  
  

  
  Why would it? You can abbreviate a false statement as much as a true statement.
  – Malice Vidrine
  Sep 5 at 0:52
  

  
  
  
  


• 
  
  
  

  
  2
  

  
  
  
  
  
  

  
  What is this "valid/makes sense" if it is not "is a well-formed formula of the language"? Why would an abbreviation need this extra condition to hold?
  – Malice Vidrine
  Sep 5 at 0:56
  

  
  
  
  


• 
  
  
  

  
  3
  

  
  
  
  
  
  

  
  The axioms don't tell you what the well formed formulas are. They tell you which ones are true. The recursive definition of a well formed formula comes prior to even stating the axioms.
  – Malice Vidrine
  Sep 5 at 0:59
  

  
  
  
  


• 
  
  
  

  
  5
  

  
  
  
  
  
  

  
  Because axioms aren't about telling us what formulas are well formed. That has never been their purpose. They tell us, combined with rules of inference, what we can prove (i.e. what will always be true if our logic is sound). This has nothing to do with defining things. This is also different than "how do we know what we're assigning to any given wff?", which also has nothing to do with defining things. How does modus ponens figure into defining things? Not at all. It figures into proving things. Your questions seem to be, instead, a great many questions about the semantics of logic.
  – Malice Vidrine
  Sep 5 at 1:34
  

  
  
  
  

 | 
show 26 more comments

up vote
4
down vote

I'm going to guess that you're conflating two different notions, namely "well-formed" and "logically valid". (My guess is admittedly based on just one little piece of one of your comments, namely "valid / makes sense".)

Of those two notions, only "well-formed" is relevant to definitions. You can define new symbols to abbreviate any well-formed formula, for example $neg(atoneg b)$. The well-formed formulas are the ones that "make sense", i.e., have a truth value once you specify truth values for the variables in them. For example (check this with a truth table if you haven't already done so), $neg(atoneg b)$ is true if both $a$ and $b$ are true, but $neg(atoneg b)$ is false in all other circumstances.

Of the two notions, only "logically valid" is governed by the axioms and inference rules. The axioms are certain, selected, logically valid formulas, and the inference rules enable us to produce additional logically valid formulas from the axioms. We'll never produce $neg(atoneg b)$ that way, because it's not logically valid. As indicated above, it's false sometimes (whenever at least one of $a$ and $b$ is false).

So $neg(atoneg b)$ is not valid, but it is well-formed. In other words, it's not always true, but it always makes sense, it always has a truth value (when $a$ and $b$ have truth values). And the latter is what's needed for the defined expression $aland b$ to make sense.

share|cite|improve this answer

answered Sep 5 at 1:43

Andreas Blass

47.8k349106

• 
  
  
  

  
  

  
  
  
  
  
  

  
  "Of those two notions, only "well-formed" is relevant to definitions." So, would you assert that if we defined (a$lor$b), where $lor$ gets understood as logical disjunction, as ¬(a→¬b) that would make sense as a definition? At the very least, that's different from conventional definitions, since conventional definitions usually preserve truth if you replace one side with another when one side appears as a subformula in some formula.
  – Doug Spoonwood
  Sep 5 at 3:20
  

  
  
  
  


• 
  
  
  

  
  

  
  
  
  
  
  

  
  @DougSpoonwood If we made that definition, we'd be introducing the symbol $lor$ to mean "and". Not a good idea, since people are accustomed to a different definition and are likely to be confused. But, in and of itself, it's a legitimate definition. (Note that people have used $sim$ to mean negation and other people have used the same symbol for biconditional. Either definition by itself is legitimate.)
  – Andreas Blass
  Sep 5 at 3:26
  

  
  
  
  


• 
  
  
  

  
  1
  

  
  
  
  
  
  

  
  @DougSpoonwood I should also say something about "where $lor$ gets understood as logical disjunction" in your comment. If we defined $lor$ in the way you described, then to understand $lor$ as logical disjunction would be to misunderstand it.
  – Andreas Blass
  Sep 5 at 3:29
  

  
  
  
  

add a comment | 

up vote
0
down vote

The key issue here is soundness.

The purpose of definitions in propositional calculus lies in converting notions not using the primitive connectives into well-formed formulas using only the primitive connectives, and doing the converse. In other words, definitions exist to translate between connectives.

There's an alternative way of expressing definitions by having a propositional calculus with functorial variables instead of a propositional calculus without functorial variables. Basically, it turns out that definitions which define connectives convert into tautologies with functorial variables of the form (in Polish notation)

C $delta$x $delta$y

where x is one-side of the definition, and y is the other-side of the definition. It also turns that if C $delta$x $delta$y, then Exy, and if Exy then C $delta$x $delta$y. Correspondingly, every definition has the property that one-side is logically equivalent to the other side of the definition. Thus, for any definition of a connective, if a well-formed formula gets written in Polish notation, the connective should appear once as the first symbol in the well-formed formula and only appear once in that well-formed formula. If some other formula equals it, then one can reasonably define that connective by that other formula.

For example, one common definition (again in Polish notation) is:

Apq := CNpq

which defines logical disjunction in terms of implication and negation. But, since

E Apq CCpqq

is a tautology also, and A appears the first symbol in 'Apq' and only appears once in 'Apq', one could use 'CCpqq' to define 'A' instead of using 'CNpq'.

To go over your questions one by one:

"Why is this permitted?"

Because anytime an instance of the formula (once parentheses get restored) on one side appears within a well-formed formula W, it can replace can get replaced by the formula (once parentheses get restored) on the right without W' changing from true to false, or from false to true. Or in short, definitional replacement preserves truth (this property is immediately evident for a formula like C $delta$x $delta$y once you understand how substitution for $delta$ works). Thus, it doesn't result in an invalidity. So, if the axioms are sound, definitional replacement preserves soundness.

"What are we allowed to define?"

Any connective can get defined in terms of formulas only having the primitive connectives of the system. This gets done to ensure that the system is adequate.

"What are we even using modus ponens and the axioms for if we can just make up whatever?"

Because only a subset or subclass of "whatever" will qualify as logically sound. Modus ponens is sound. So are the axioms. The definitions also either are sound, or work out as consistent with soundness. So again, the key issue here is soundness.

share|cite|improve this answer

answered Sep 5 at 3:15

Doug Spoonwood

7,82412043

add a comment | 

Your Answer

StackExchange.ifUsing("editor", function ()
return StackExchange.using("mathjaxEditing", function ()
StackExchange.MarkdownEditor.creationCallbacks.add(function (editor, postfix)
StackExchange.mathjaxEditing.prepareWmdForMathJax(editor, postfix, [["$", "$"], ["\\(","\\)"]]);
);
);
, "mathjax-editing");

StackExchange.ready(function()
var channelOptions =
tags: "".split(" "),
id: "69"
;
initTagRenderer("".split(" "), "".split(" "), channelOptions);

StackExchange.using("externalEditor", function()
// Have to fire editor after snippets, if snippets enabled
if (StackExchange.settings.snippets.snippetsEnabled)
StackExchange.using("snippets", function()
createEditor();
);

else
createEditor();

);

function createEditor()
StackExchange.prepareEditor(
heartbeatType: 'answer',
convertImagesToLinks: true,
noModals: false,
showLowRepImageUploadWarning: true,
reputationToPostImages: 10,
bindNavPrevention: true,
postfix: "",
noCode: true, onDemand: true,
discardSelector: ".discard-answer"
,immediatelyShowMarkdownHelp:true
);



);

 

draft saved

draft discarded

Sign up or log in

StackExchange.ready(function ()
StackExchange.helpers.onClickDraftSave('#login-link');
);

Sign up using Google

Sign up using Facebook

Sign up using Email and Password

Post as a guest

Name Email

StackExchange.ready(
function ()
StackExchange.openid.initPostLogin('.new-post-login', 'https%3a%2f%2fmath.stackexchange.com%2fquestions%2f2905685%2fdo-definitions-have-to-fit-axioms-in-logic%23new-answer', 'question_page');

);

Post as a guest

Name Email

4 Answers
4

active

oldest

votes

4 Answers
4

active

oldest

votes

active

oldest

votes

active

oldest

votes

up vote
4
down vote



accepted

Your question arises from the failure of many texts in properly distinguishing between the meta-system and the actual formal system under study. You, at all times, are doing mathematics in the meta-system, and in the field of mathematical logic you are studying some formal system (such as the one you have here with some syntactic rules for forming well-formed formulae (wff) and one deductive rule and three axioms). So, let us precisely express them, and you will see.
$
defquote#1``#1"
defmeta#1mathbindot#1
$

Syntactic rules

Note that wffs are strings. Given any two strings $x,y$ we shall use "$x+y$" to denote the concatenation of $x$ followed by $y$. We shall also use quotes to specify literal strings. For example, you are a person but "you" is a string.

Closure under negation: Given any wff $A$, the string $quoteneg+A$ is also a wff.

Closure under implication: Given any wffs $A,B$, the string $quote(+A+quoteto+B+quote)$ is also a wff.

Note how I used quote-marks above. It would be technically incorrect to write:

... the string $(A to B)$ is also a wff. (technically incorrect)

Because the "$to$" and the brackets are symbols in the formal system under study, not symbols in the meta-system we are using!

Deductive rules

The system under study has only one deductive rule:

Given any wffs P,Q, if you have deduced $P$ and $quote(+P+quoteto+Q+quote)$, then you can deduce $Q$.

Again, note how I used quote-marks.

Abbreviative definitions

Now we come to the so-called 'definition' of "$land$":

Take any strings $A,B$. The string $quote(+A+quoteland+B+quote)$ is not a wff in the formal system under study, simply because "$land$" is not a symbol in its language. However, we wish to use that string to stand for $quoteneg(+A+quotetoneg+B+quote)$.

This wish is not trivial to fulfill rigorously. The easiest way to do it correctly is to add a syntactic rule for closure of wffs under $quoteland$:

Closure under conjunction: Given any wffs $A,B$, the string $quote(+A+quoteland+B+quote)$ is also a wff.

and then check that you can still uniquely parse (interpret) a wff, so that it makes sense to stipulate that $quote(+A+quoteland+B+quote)$ is rewritten as $quoteneg(+A+quotetoneg+B+quote)$ before parsing, to obtain our wish.

As you observed, such a rewrite-rule is not an axiom.

What is that 'equality'?

Note that I did not say that $quote(+A+quoteland+B+quote)$ is the same string as $quoteneg(+A+quotetoneg+B+quote)$, because it is of course false. We are only using a rewrite-rule; the strings themselves are not equal.

You are equally free to 'define' any other notation in the same fashion, using rewrite-rules, and you would have to deal with the same issue of unique parsing. This happens in mathematics itself as well. When you define a new notation it is important that there is still only one way to read things.

So while it is technically wrong to state this rewrite-rule as an equality, it is intuitively 'equal' in the sense of being logically equivalent, since the final parsing is the same.

---

I hope that this addresses your inquiry. If everything is clear, you can continue reading. There is a different way to go about logic that would actually make what is technically wrong above correct, but it may be confusing unless you fully understand the more concrete way above.

Meta-operators

First let us see how we can abstract out the wff formation:

Given any string $A$, define $metaneg A = quoteneg+A$.

Given any strings $A,B$, define $A metato B = quote(+A+quoteto+B+quote)$.

Note that unlike the strings $quoteneg$ and $quoteto$, $metaneg$ and $metato$ are operations on strings (in the meta-system). So we can in fact do the following:

Given any strings $A,B$, define $A metaland B = metaneg( A metato (metaneg B) )$.

Note that the brackets here are in the meta-system, used so that we know which string operation to perform first. If we use the typical precedence rules, namely that $metaneg$ is higher precedence than $metato$, then we could have done the following:

Given any strings $A,B$, define $A metaland B = metaneg( A metato metaneg B )$.

A more abstract way to conceptualize this is that $metato$ and $metaneg$ are actually operations on parse trees rather than strings, and so the above definition of $metaland$ is just a definition of a new operation on parse trees in terms of previously defined ones.

The question that may arise at this point is: Why don't we do it this way and not use strings at all? The simple answer is that the only way to completely formalize a formal system is to be able to encode it into some linear representation such as strings, so you are still going to have to decide on how exactly to encode wffs as strings. Similarly when you use logic on paper. Hence the concrete first approach is ultimately the practical way.

share|cite|improve this answer

answered Sep 5 at 4:52

user21820

36.2k440140

add a comment | 

up vote
4
down vote



accepted

Your question arises from the failure of many texts in properly distinguishing between the meta-system and the actual formal system under study. You, at all times, are doing mathematics in the meta-system, and in the field of mathematical logic you are studying some formal system (such as the one you have here with some syntactic rules for forming well-formed formulae (wff) and one deductive rule and three axioms). So, let us precisely express them, and you will see.
$
defquote#1``#1"
defmeta#1mathbindot#1
$

Syntactic rules

Note that wffs are strings. Given any two strings $x,y$ we shall use "$x+y$" to denote the concatenation of $x$ followed by $y$. We shall also use quotes to specify literal strings. For example, you are a person but "you" is a string.

Closure under negation: Given any wff $A$, the string $quoteneg+A$ is also a wff.

Closure under implication: Given any wffs $A,B$, the string $quote(+A+quoteto+B+quote)$ is also a wff.

Note how I used quote-marks above. It would be technically incorrect to write:

... the string $(A to B)$ is also a wff. (technically incorrect)

Because the "$to$" and the brackets are symbols in the formal system under study, not symbols in the meta-system we are using!

Deductive rules

The system under study has only one deductive rule:

Given any wffs P,Q, if you have deduced $P$ and $quote(+P+quoteto+Q+quote)$, then you can deduce $Q$.

Again, note how I used quote-marks.

Abbreviative definitions

Now we come to the so-called 'definition' of "$land$":

Take any strings $A,B$. The string $quote(+A+quoteland+B+quote)$ is not a wff in the formal system under study, simply because "$land$" is not a symbol in its language. However, we wish to use that string to stand for $quoteneg(+A+quotetoneg+B+quote)$.

This wish is not trivial to fulfill rigorously. The easiest way to do it correctly is to add a syntactic rule for closure of wffs under $quoteland$:

Closure under conjunction: Given any wffs $A,B$, the string $quote(+A+quoteland+B+quote)$ is also a wff.

and then check that you can still uniquely parse (interpret) a wff, so that it makes sense to stipulate that $quote(+A+quoteland+B+quote)$ is rewritten as $quoteneg(+A+quotetoneg+B+quote)$ before parsing, to obtain our wish.

As you observed, such a rewrite-rule is not an axiom.

What is that 'equality'?

Note that I did not say that $quote(+A+quoteland+B+quote)$ is the same string as $quoteneg(+A+quotetoneg+B+quote)$, because it is of course false. We are only using a rewrite-rule; the strings themselves are not equal.

You are equally free to 'define' any other notation in the same fashion, using rewrite-rules, and you would have to deal with the same issue of unique parsing. This happens in mathematics itself as well. When you define a new notation it is important that there is still only one way to read things.

So while it is technically wrong to state this rewrite-rule as an equality, it is intuitively 'equal' in the sense of being logically equivalent, since the final parsing is the same.

---

I hope that this addresses your inquiry. If everything is clear, you can continue reading. There is a different way to go about logic that would actually make what is technically wrong above correct, but it may be confusing unless you fully understand the more concrete way above.

Meta-operators

First let us see how we can abstract out the wff formation:

Given any string $A$, define $metaneg A = quoteneg+A$.

Given any strings $A,B$, define $A metato B = quote(+A+quoteto+B+quote)$.

Note that unlike the strings $quoteneg$ and $quoteto$, $metaneg$ and $metato$ are operations on strings (in the meta-system). So we can in fact do the following:

Given any strings $A,B$, define $A metaland B = metaneg( A metato (metaneg B) )$.

Note that the brackets here are in the meta-system, used so that we know which string operation to perform first. If we use the typical precedence rules, namely that $metaneg$ is higher precedence than $metato$, then we could have done the following:

Given any strings $A,B$, define $A metaland B = metaneg( A metato metaneg B )$.

A more abstract way to conceptualize this is that $metato$ and $metaneg$ are actually operations on parse trees rather than strings, and so the above definition of $metaland$ is just a definition of a new operation on parse trees in terms of previously defined ones.

The question that may arise at this point is: Why don't we do it this way and not use strings at all? The simple answer is that the only way to completely formalize a formal system is to be able to encode it into some linear representation such as strings, so you are still going to have to decide on how exactly to encode wffs as strings. Similarly when you use logic on paper. Hence the concrete first approach is ultimately the practical way.

share|cite|improve this answer

answered Sep 5 at 4:52

user21820

36.2k440140

add a comment | 

up vote
4
down vote



accepted

up vote
4
down vote



accepted

Your question arises from the failure of many texts in properly distinguishing between the meta-system and the actual formal system under study. You, at all times, are doing mathematics in the meta-system, and in the field of mathematical logic you are studying some formal system (such as the one you have here with some syntactic rules for forming well-formed formulae (wff) and one deductive rule and three axioms). So, let us precisely express them, and you will see.
$
defquote#1``#1"
defmeta#1mathbindot#1
$

Syntactic rules

Note that wffs are strings. Given any two strings $x,y$ we shall use "$x+y$" to denote the concatenation of $x$ followed by $y$. We shall also use quotes to specify literal strings. For example, you are a person but "you" is a string.

Closure under negation: Given any wff $A$, the string $quoteneg+A$ is also a wff.

Closure under implication: Given any wffs $A,B$, the string $quote(+A+quoteto+B+quote)$ is also a wff.

Note how I used quote-marks above. It would be technically incorrect to write:

... the string $(A to B)$ is also a wff. (technically incorrect)

Because the "$to$" and the brackets are symbols in the formal system under study, not symbols in the meta-system we are using!

Deductive rules

The system under study has only one deductive rule:

Given any wffs P,Q, if you have deduced $P$ and $quote(+P+quoteto+Q+quote)$, then you can deduce $Q$.

Again, note how I used quote-marks.

Abbreviative definitions

Now we come to the so-called 'definition' of "$land$":

Take any strings $A,B$. The string $quote(+A+quoteland+B+quote)$ is not a wff in the formal system under study, simply because "$land$" is not a symbol in its language. However, we wish to use that string to stand for $quoteneg(+A+quotetoneg+B+quote)$.

This wish is not trivial to fulfill rigorously. The easiest way to do it correctly is to add a syntactic rule for closure of wffs under $quoteland$:

Closure under conjunction: Given any wffs $A,B$, the string $quote(+A+quoteland+B+quote)$ is also a wff.

and then check that you can still uniquely parse (interpret) a wff, so that it makes sense to stipulate that $quote(+A+quoteland+B+quote)$ is rewritten as $quoteneg(+A+quotetoneg+B+quote)$ before parsing, to obtain our wish.

As you observed, such a rewrite-rule is not an axiom.

What is that 'equality'?

Note that I did not say that $quote(+A+quoteland+B+quote)$ is the same string as $quoteneg(+A+quotetoneg+B+quote)$, because it is of course false. We are only using a rewrite-rule; the strings themselves are not equal.

You are equally free to 'define' any other notation in the same fashion, using rewrite-rules, and you would have to deal with the same issue of unique parsing. This happens in mathematics itself as well. When you define a new notation it is important that there is still only one way to read things.

So while it is technically wrong to state this rewrite-rule as an equality, it is intuitively 'equal' in the sense of being logically equivalent, since the final parsing is the same.

---

I hope that this addresses your inquiry. If everything is clear, you can continue reading. There is a different way to go about logic that would actually make what is technically wrong above correct, but it may be confusing unless you fully understand the more concrete way above.

Meta-operators

First let us see how we can abstract out the wff formation:

Given any string $A$, define $metaneg A = quoteneg+A$.

Given any strings $A,B$, define $A metato B = quote(+A+quoteto+B+quote)$.

Note that unlike the strings $quoteneg$ and $quoteto$, $metaneg$ and $metato$ are operations on strings (in the meta-system). So we can in fact do the following:

Given any strings $A,B$, define $A metaland B = metaneg( A metato (metaneg B) )$.

Note that the brackets here are in the meta-system, used so that we know which string operation to perform first. If we use the typical precedence rules, namely that $metaneg$ is higher precedence than $metato$, then we could have done the following:

Given any strings $A,B$, define $A metaland B = metaneg( A metato metaneg B )$.

A more abstract way to conceptualize this is that $metato$ and $metaneg$ are actually operations on parse trees rather than strings, and so the above definition of $metaland$ is just a definition of a new operation on parse trees in terms of previously defined ones.

The question that may arise at this point is: Why don't we do it this way and not use strings at all? The simple answer is that the only way to completely formalize a formal system is to be able to encode it into some linear representation such as strings, so you are still going to have to decide on how exactly to encode wffs as strings. Similarly when you use logic on paper. Hence the concrete first approach is ultimately the practical way.

share|cite|improve this answer

answered Sep 5 at 4:52

user21820

36.2k440140

Your question arises from the failure of many texts in properly distinguishing between the meta-system and the actual formal system under study. You, at all times, are doing mathematics in the meta-system, and in the field of mathematical logic you are studying some formal system (such as the one you have here with some syntactic rules for forming well-formed formulae (wff) and one deductive rule and three axioms). So, let us precisely express them, and you will see.
$
defquote#1``#1"
defmeta#1mathbindot#1
$

Syntactic rules

Note that wffs are strings. Given any two strings $x,y$ we shall use "$x+y$" to denote the concatenation of $x$ followed by $y$. We shall also use quotes to specify literal strings. For example, you are a person but "you" is a string.

Closure under negation: Given any wff $A$, the string $quoteneg+A$ is also a wff.

Closure under implication: Given any wffs $A,B$, the string $quote(+A+quoteto+B+quote)$ is also a wff.

Note how I used quote-marks above. It would be technically incorrect to write:

... the string $(A to B)$ is also a wff. (technically incorrect)

Because the "$to$" and the brackets are symbols in the formal system under study, not symbols in the meta-system we are using!

Deductive rules

The system under study has only one deductive rule:

Given any wffs P,Q, if you have deduced $P$ and $quote(+P+quoteto+Q+quote)$, then you can deduce $Q$.

Again, note how I used quote-marks.

Abbreviative definitions

Now we come to the so-called 'definition' of "$land$":

Take any strings $A,B$. The string $quote(+A+quoteland+B+quote)$ is not a wff in the formal system under study, simply because "$land$" is not a symbol in its language. However, we wish to use that string to stand for $quoteneg(+A+quotetoneg+B+quote)$.

This wish is not trivial to fulfill rigorously. The easiest way to do it correctly is to add a syntactic rule for closure of wffs under $quoteland$:

Closure under conjunction: Given any wffs $A,B$, the string $quote(+A+quoteland+B+quote)$ is also a wff.

and then check that you can still uniquely parse (interpret) a wff, so that it makes sense to stipulate that $quote(+A+quoteland+B+quote)$ is rewritten as $quoteneg(+A+quotetoneg+B+quote)$ before parsing, to obtain our wish.

As you observed, such a rewrite-rule is not an axiom.

What is that 'equality'?

Note that I did not say that $quote(+A+quoteland+B+quote)$ is the same string as $quoteneg(+A+quotetoneg+B+quote)$, because it is of course false. We are only using a rewrite-rule; the strings themselves are not equal.

You are equally free to 'define' any other notation in the same fashion, using rewrite-rules, and you would have to deal with the same issue of unique parsing. This happens in mathematics itself as well. When you define a new notation it is important that there is still only one way to read things.

So while it is technically wrong to state this rewrite-rule as an equality, it is intuitively 'equal' in the sense of being logically equivalent, since the final parsing is the same.

---

I hope that this addresses your inquiry. If everything is clear, you can continue reading. There is a different way to go about logic that would actually make what is technically wrong above correct, but it may be confusing unless you fully understand the more concrete way above.

Meta-operators

First let us see how we can abstract out the wff formation:

Given any string $A$, define $metaneg A = quoteneg+A$.

Given any strings $A,B$, define $A metato B = quote(+A+quoteto+B+quote)$.

Note that unlike the strings $quoteneg$ and $quoteto$, $metaneg$ and $metato$ are operations on strings (in the meta-system). So we can in fact do the following:

Given any strings $A,B$, define $A metaland B = metaneg( A metato (metaneg B) )$.

Note that the brackets here are in the meta-system, used so that we know which string operation to perform first. If we use the typical precedence rules, namely that $metaneg$ is higher precedence than $metato$, then we could have done the following:

Given any strings $A,B$, define $A metaland B = metaneg( A metato metaneg B )$.

A more abstract way to conceptualize this is that $metato$ and $metaneg$ are actually operations on parse trees rather than strings, and so the above definition of $metaland$ is just a definition of a new operation on parse trees in terms of previously defined ones.

The question that may arise at this point is: Why don't we do it this way and not use strings at all? The simple answer is that the only way to completely formalize a formal system is to be able to encode it into some linear representation such as strings, so you are still going to have to decide on how exactly to encode wffs as strings. Similarly when you use logic on paper. Hence the concrete first approach is ultimately the practical way.

share|cite|improve this answer

answered Sep 5 at 4:52

user21820

36.2k440140

share|cite|improve this answer

share|cite|improve this answer

answered Sep 5 at 4:52

user21820

36.2k440140

answered Sep 5 at 4:52

user21820

36.2k440140

answered Sep 5 at 4:52

user21820

36.2k440140

36.2k440140

add a comment | 

add a comment | 

up vote
8
down vote

You can define anything you want. However, the point of defining something is to make it easier to refer to, which means that the most useful definitions are for things that are:

(a) frequently referred to;

(b) not trivial; and often

(c) similar to something else

So, for example, we define $wedge$ because it allows for a lot of shortcuts in writing the propositional logic, and it happens to align with the general understanding of the word "and". The "=" in the definition isn't really part of the logic, it's a part of the language surrounding it, and we know that there's a level at which we have to resort to shared understanding since you can only abstract things so far.

On the other hand, I probably wouldn't bother coming up with a definition for "the set of all even prime numbers in $mathbbN$", because it's simple enough to just say $2$. Or if I did define it, it would only be for a very limited context (for example, one where I actually needed to prove that 2 is the only element in the set), so I could get away with a generic definition like $A$.

share|cite|improve this answer

answered Sep 4 at 23:43

ConMan

7,1861324

• 
  
  
  

  
  5
  

  
  
  
  
  
  

  
  @user525966 - The only thing that hasn't been mentioned, because I believe it was presumed clear, is that such definitions are just informal abbreviations. I hope it doesn't need explanation that using a shorthand for an expression doesn't require us to know about, and doesn't change anything about, whether that expression is true or not.
  – Malice Vidrine
  Sep 5 at 0:38
  

  
  
  
  


• 
  
  
  

  
  2
  

  
  
  
  
  
  

  
  Why would it? You can abbreviate a false statement as much as a true statement.
  – Malice Vidrine
  Sep 5 at 0:52
  

  
  
  
  


• 
  
  
  

  
  2
  

  
  
  
  
  
  

  
  What is this "valid/makes sense" if it is not "is a well-formed formula of the language"? Why would an abbreviation need this extra condition to hold?
  – Malice Vidrine
  Sep 5 at 0:56
  

  
  
  
  


• 
  
  
  

  
  3
  

  
  
  
  
  
  

  
  The axioms don't tell you what the well formed formulas are. They tell you which ones are true. The recursive definition of a well formed formula comes prior to even stating the axioms.
  – Malice Vidrine
  Sep 5 at 0:59
  

  
  
  
  


• 
  
  
  

  
  5
  

  
  
  
  
  
  

  
  Because axioms aren't about telling us what formulas are well formed. That has never been their purpose. They tell us, combined with rules of inference, what we can prove (i.e. what will always be true if our logic is sound). This has nothing to do with defining things. This is also different than "how do we know what we're assigning to any given wff?", which also has nothing to do with defining things. How does modus ponens figure into defining things? Not at all. It figures into proving things. Your questions seem to be, instead, a great many questions about the semantics of logic.
  – Malice Vidrine
  Sep 5 at 1:34
  

  
  
  
  

 | 
show 26 more comments

up vote
8
down vote

You can define anything you want. However, the point of defining something is to make it easier to refer to, which means that the most useful definitions are for things that are:

(a) frequently referred to;

(b) not trivial; and often

(c) similar to something else

So, for example, we define $wedge$ because it allows for a lot of shortcuts in writing the propositional logic, and it happens to align with the general understanding of the word "and". The "=" in the definition isn't really part of the logic, it's a part of the language surrounding it, and we know that there's a level at which we have to resort to shared understanding since you can only abstract things so far.

On the other hand, I probably wouldn't bother coming up with a definition for "the set of all even prime numbers in $mathbbN$", because it's simple enough to just say $2$. Or if I did define it, it would only be for a very limited context (for example, one where I actually needed to prove that 2 is the only element in the set), so I could get away with a generic definition like $A$.

share|cite|improve this answer

answered Sep 4 at 23:43

ConMan

7,1861324

• 
  
  
  

  
  5
  

  
  
  
  
  
  

  
  @user525966 - The only thing that hasn't been mentioned, because I believe it was presumed clear, is that such definitions are just informal abbreviations. I hope it doesn't need explanation that using a shorthand for an expression doesn't require us to know about, and doesn't change anything about, whether that expression is true or not.
  – Malice Vidrine
  Sep 5 at 0:38
  

  
  
  
  


• 
  
  
  

  
  2
  

  
  
  
  
  
  

  
  Why would it? You can abbreviate a false statement as much as a true statement.
  – Malice Vidrine
  Sep 5 at 0:52
  

  
  
  
  


• 
  
  
  

  
  2
  

  
  
  
  
  
  

  
  What is this "valid/makes sense" if it is not "is a well-formed formula of the language"? Why would an abbreviation need this extra condition to hold?
  – Malice Vidrine
  Sep 5 at 0:56
  

  
  
  
  


• 
  
  
  

  
  3
  

  
  
  
  
  
  

  
  The axioms don't tell you what the well formed formulas are. They tell you which ones are true. The recursive definition of a well formed formula comes prior to even stating the axioms.
  – Malice Vidrine
  Sep 5 at 0:59
  

  
  
  
  


• 
  
  
  

  
  5
  

  
  
  
  
  
  

  
  Because axioms aren't about telling us what formulas are well formed. That has never been their purpose. They tell us, combined with rules of inference, what we can prove (i.e. what will always be true if our logic is sound). This has nothing to do with defining things. This is also different than "how do we know what we're assigning to any given wff?", which also has nothing to do with defining things. How does modus ponens figure into defining things? Not at all. It figures into proving things. Your questions seem to be, instead, a great many questions about the semantics of logic.
  – Malice Vidrine
  Sep 5 at 1:34
  

  
  
  
  

 | 
show 26 more comments

up vote
8
down vote

up vote
8
down vote

You can define anything you want. However, the point of defining something is to make it easier to refer to, which means that the most useful definitions are for things that are:

(a) frequently referred to;

(b) not trivial; and often

(c) similar to something else

So, for example, we define $wedge$ because it allows for a lot of shortcuts in writing the propositional logic, and it happens to align with the general understanding of the word "and". The "=" in the definition isn't really part of the logic, it's a part of the language surrounding it, and we know that there's a level at which we have to resort to shared understanding since you can only abstract things so far.

On the other hand, I probably wouldn't bother coming up with a definition for "the set of all even prime numbers in $mathbbN$", because it's simple enough to just say $2$. Or if I did define it, it would only be for a very limited context (for example, one where I actually needed to prove that 2 is the only element in the set), so I could get away with a generic definition like $A$.

share|cite|improve this answer

answered Sep 4 at 23:43

ConMan

7,1861324

You can define anything you want. However, the point of defining something is to make it easier to refer to, which means that the most useful definitions are for things that are:

(a) frequently referred to;

(b) not trivial; and often

(c) similar to something else

So, for example, we define $wedge$ because it allows for a lot of shortcuts in writing the propositional logic, and it happens to align with the general understanding of the word "and". The "=" in the definition isn't really part of the logic, it's a part of the language surrounding it, and we know that there's a level at which we have to resort to shared understanding since you can only abstract things so far.

On the other hand, I probably wouldn't bother coming up with a definition for "the set of all even prime numbers in $mathbbN$", because it's simple enough to just say $2$. Or if I did define it, it would only be for a very limited context (for example, one where I actually needed to prove that 2 is the only element in the set), so I could get away with a generic definition like $A$.

share|cite|improve this answer

answered Sep 4 at 23:43

ConMan

7,1861324

share|cite|improve this answer

share|cite|improve this answer

answered Sep 4 at 23:43

ConMan

7,1861324

answered Sep 4 at 23:43

ConMan

7,1861324

answered Sep 4 at 23:43

ConMan

7,1861324

7,1861324

• 
  
  
  

  
  5
  

  
  
  
  
  
  

  
  @user525966 - The only thing that hasn't been mentioned, because I believe it was presumed clear, is that such definitions are just informal abbreviations. I hope it doesn't need explanation that using a shorthand for an expression doesn't require us to know about, and doesn't change anything about, whether that expression is true or not.
  – Malice Vidrine
  Sep 5 at 0:38
  

  
  
  
  


• 
  
  
  

  
  2
  

  
  
  
  
  
  

  
  Why would it? You can abbreviate a false statement as much as a true statement.
  – Malice Vidrine
  Sep 5 at 0:52
  

  
  
  
  


• 
  
  
  

  
  2
  

  
  
  
  
  
  

  
  What is this "valid/makes sense" if it is not "is a well-formed formula of the language"? Why would an abbreviation need this extra condition to hold?
  – Malice Vidrine
  Sep 5 at 0:56
  

  
  
  
  


• 
  
  
  

  
  3
  

  
  
  
  
  
  

  
  The axioms don't tell you what the well formed formulas are. They tell you which ones are true. The recursive definition of a well formed formula comes prior to even stating the axioms.
  – Malice Vidrine
  Sep 5 at 0:59
  

  
  
  
  


• 
  
  
  

  
  5
  

  
  
  
  
  
  

  
  Because axioms aren't about telling us what formulas are well formed. That has never been their purpose. They tell us, combined with rules of inference, what we can prove (i.e. what will always be true if our logic is sound). This has nothing to do with defining things. This is also different than "how do we know what we're assigning to any given wff?", which also has nothing to do with defining things. How does modus ponens figure into defining things? Not at all. It figures into proving things. Your questions seem to be, instead, a great many questions about the semantics of logic.
  – Malice Vidrine
  Sep 5 at 1:34
  

  
  
  
  

 | 
show 26 more comments

• 
  
  
  

  
  5
  

  
  
  
  
  
  

  
  @user525966 - The only thing that hasn't been mentioned, because I believe it was presumed clear, is that such definitions are just informal abbreviations. I hope it doesn't need explanation that using a shorthand for an expression doesn't require us to know about, and doesn't change anything about, whether that expression is true or not.
  – Malice Vidrine
  Sep 5 at 0:38
  

  
  
  
  


• 
  
  
  

  
  2
  

  
  
  
  
  
  

  
  Why would it? You can abbreviate a false statement as much as a true statement.
  – Malice Vidrine
  Sep 5 at 0:52
  

  
  
  
  


• 
  
  
  

  
  2
  

  
  
  
  
  
  

  
  What is this "valid/makes sense" if it is not "is a well-formed formula of the language"? Why would an abbreviation need this extra condition to hold?
  – Malice Vidrine
  Sep 5 at 0:56
  

  
  
  
  


• 
  
  
  

  
  3
  

  
  
  
  
  
  

  
  The axioms don't tell you what the well formed formulas are. They tell you which ones are true. The recursive definition of a well formed formula comes prior to even stating the axioms.
  – Malice Vidrine
  Sep 5 at 0:59
  

  
  
  
  


• 
  
  
  

  
  5
  

  
  
  
  
  
  

  
  Because axioms aren't about telling us what formulas are well formed. That has never been their purpose. They tell us, combined with rules of inference, what we can prove (i.e. what will always be true if our logic is sound). This has nothing to do with defining things. This is also different than "how do we know what we're assigning to any given wff?", which also has nothing to do with defining things. How does modus ponens figure into defining things? Not at all. It figures into proving things. Your questions seem to be, instead, a great many questions about the semantics of logic.
  – Malice Vidrine
  Sep 5 at 1:34
  

  
  
  
  

5

5

@user525966 - The only thing that hasn't been mentioned, because I believe it was presumed clear, is that such definitions are just informal abbreviations. I hope it doesn't need explanation that using a shorthand for an expression doesn't require us to know about, and doesn't change anything about, whether that expression is true or not.
– Malice Vidrine
Sep 5 at 0:38

@user525966 - The only thing that hasn't been mentioned, because I believe it was presumed clear, is that such definitions are just informal abbreviations. I hope it doesn't need explanation that using a shorthand for an expression doesn't require us to know about, and doesn't change anything about, whether that expression is true or not.
– Malice Vidrine
Sep 5 at 0:38

2

2

Why would it? You can abbreviate a false statement as much as a true statement.
– Malice Vidrine
Sep 5 at 0:52

Why would it? You can abbreviate a false statement as much as a true statement.
– Malice Vidrine
Sep 5 at 0:52

2

2

What is this "valid/makes sense" if it is not "is a well-formed formula of the language"? Why would an abbreviation need this extra condition to hold?
– Malice Vidrine
Sep 5 at 0:56

What is this "valid/makes sense" if it is not "is a well-formed formula of the language"? Why would an abbreviation need this extra condition to hold?
– Malice Vidrine
Sep 5 at 0:56

3

3

The axioms don't tell you what the well formed formulas are. They tell you which ones are true. The recursive definition of a well formed formula comes prior to even stating the axioms.
– Malice Vidrine
Sep 5 at 0:59

The axioms don't tell you what the well formed formulas are. They tell you which ones are true. The recursive definition of a well formed formula comes prior to even stating the axioms.
– Malice Vidrine
Sep 5 at 0:59

5

5

Because axioms aren't about telling us what formulas are well formed. That has never been their purpose. They tell us, combined with rules of inference, what we can prove (i.e. what will always be true if our logic is sound). This has nothing to do with defining things. This is also different than "how do we know what we're assigning to any given wff?", which also has nothing to do with defining things. How does modus ponens figure into defining things? Not at all. It figures into proving things. Your questions seem to be, instead, a great many questions about the semantics of logic.
– Malice Vidrine
Sep 5 at 1:34

Because axioms aren't about telling us what formulas are well formed. That has never been their purpose. They tell us, combined with rules of inference, what we can prove (i.e. what will always be true if our logic is sound). This has nothing to do with defining things. This is also different than "how do we know what we're assigning to any given wff?", which also has nothing to do with defining things. How does modus ponens figure into defining things? Not at all. It figures into proving things. Your questions seem to be, instead, a great many questions about the semantics of logic.
– Malice Vidrine
Sep 5 at 1:34

 | 
show 26 more comments

up vote
4
down vote

I'm going to guess that you're conflating two different notions, namely "well-formed" and "logically valid". (My guess is admittedly based on just one little piece of one of your comments, namely "valid / makes sense".)

Of those two notions, only "well-formed" is relevant to definitions. You can define new symbols to abbreviate any well-formed formula, for example $neg(atoneg b)$. The well-formed formulas are the ones that "make sense", i.e., have a truth value once you specify truth values for the variables in them. For example (check this with a truth table if you haven't already done so), $neg(atoneg b)$ is true if both $a$ and $b$ are true, but $neg(atoneg b)$ is false in all other circumstances.

Of the two notions, only "logically valid" is governed by the axioms and inference rules. The axioms are certain, selected, logically valid formulas, and the inference rules enable us to produce additional logically valid formulas from the axioms. We'll never produce $neg(atoneg b)$ that way, because it's not logically valid. As indicated above, it's false sometimes (whenever at least one of $a$ and $b$ is false).

So $neg(atoneg b)$ is not valid, but it is well-formed. In other words, it's not always true, but it always makes sense, it always has a truth value (when $a$ and $b$ have truth values). And the latter is what's needed for the defined expression $aland b$ to make sense.

share|cite|improve this answer

answered Sep 5 at 1:43

Andreas Blass

47.8k349106

• 
  
  
  

  
  

  
  
  
  
  
  

  
  "Of those two notions, only "well-formed" is relevant to definitions." So, would you assert that if we defined (a$lor$b), where $lor$ gets understood as logical disjunction, as ¬(a→¬b) that would make sense as a definition? At the very least, that's different from conventional definitions, since conventional definitions usually preserve truth if you replace one side with another when one side appears as a subformula in some formula.
  – Doug Spoonwood
  Sep 5 at 3:20
  

  
  
  
  


• 
  
  
  

  
  

  
  
  
  
  
  

  
  @DougSpoonwood If we made that definition, we'd be introducing the symbol $lor$ to mean "and". Not a good idea, since people are accustomed to a different definition and are likely to be confused. But, in and of itself, it's a legitimate definition. (Note that people have used $sim$ to mean negation and other people have used the same symbol for biconditional. Either definition by itself is legitimate.)
  – Andreas Blass
  Sep 5 at 3:26
  

  
  
  
  


• 
  
  
  

  
  1
  

  
  
  
  
  
  

  
  @DougSpoonwood I should also say something about "where $lor$ gets understood as logical disjunction" in your comment. If we defined $lor$ in the way you described, then to understand $lor$ as logical disjunction would be to misunderstand it.
  – Andreas Blass
  Sep 5 at 3:29
  

  
  
  
  

add a comment | 

up vote
4
down vote

I'm going to guess that you're conflating two different notions, namely "well-formed" and "logically valid". (My guess is admittedly based on just one little piece of one of your comments, namely "valid / makes sense".)

Of those two notions, only "well-formed" is relevant to definitions. You can define new symbols to abbreviate any well-formed formula, for example $neg(atoneg b)$. The well-formed formulas are the ones that "make sense", i.e., have a truth value once you specify truth values for the variables in them. For example (check this with a truth table if you haven't already done so), $neg(atoneg b)$ is true if both $a$ and $b$ are true, but $neg(atoneg b)$ is false in all other circumstances.

Of the two notions, only "logically valid" is governed by the axioms and inference rules. The axioms are certain, selected, logically valid formulas, and the inference rules enable us to produce additional logically valid formulas from the axioms. We'll never produce $neg(atoneg b)$ that way, because it's not logically valid. As indicated above, it's false sometimes (whenever at least one of $a$ and $b$ is false).

So $neg(atoneg b)$ is not valid, but it is well-formed. In other words, it's not always true, but it always makes sense, it always has a truth value (when $a$ and $b$ have truth values). And the latter is what's needed for the defined expression $aland b$ to make sense.

share|cite|improve this answer

answered Sep 5 at 1:43

Andreas Blass

47.8k349106

• 
  
  
  

  
  

  
  
  
  
  
  

  
  "Of those two notions, only "well-formed" is relevant to definitions." So, would you assert that if we defined (a$lor$b), where $lor$ gets understood as logical disjunction, as ¬(a→¬b) that would make sense as a definition? At the very least, that's different from conventional definitions, since conventional definitions usually preserve truth if you replace one side with another when one side appears as a subformula in some formula.
  – Doug Spoonwood
  Sep 5 at 3:20
  

  
  
  
  


• 
  
  
  

  
  

  
  
  
  
  
  

  
  @DougSpoonwood If we made that definition, we'd be introducing the symbol $lor$ to mean "and". Not a good idea, since people are accustomed to a different definition and are likely to be confused. But, in and of itself, it's a legitimate definition. (Note that people have used $sim$ to mean negation and other people have used the same symbol for biconditional. Either definition by itself is legitimate.)
  – Andreas Blass
  Sep 5 at 3:26
  

  
  
  
  


• 
  
  
  

  
  1
  

  
  
  
  
  
  

  
  @DougSpoonwood I should also say something about "where $lor$ gets understood as logical disjunction" in your comment. If we defined $lor$ in the way you described, then to understand $lor$ as logical disjunction would be to misunderstand it.
  – Andreas Blass
  Sep 5 at 3:29
  

  
  
  
  

add a comment | 

up vote
4
down vote

up vote
4
down vote

I'm going to guess that you're conflating two different notions, namely "well-formed" and "logically valid". (My guess is admittedly based on just one little piece of one of your comments, namely "valid / makes sense".)

Of those two notions, only "well-formed" is relevant to definitions. You can define new symbols to abbreviate any well-formed formula, for example $neg(atoneg b)$. The well-formed formulas are the ones that "make sense", i.e., have a truth value once you specify truth values for the variables in them. For example (check this with a truth table if you haven't already done so), $neg(atoneg b)$ is true if both $a$ and $b$ are true, but $neg(atoneg b)$ is false in all other circumstances.

Of the two notions, only "logically valid" is governed by the axioms and inference rules. The axioms are certain, selected, logically valid formulas, and the inference rules enable us to produce additional logically valid formulas from the axioms. We'll never produce $neg(atoneg b)$ that way, because it's not logically valid. As indicated above, it's false sometimes (whenever at least one of $a$ and $b$ is false).

So $neg(atoneg b)$ is not valid, but it is well-formed. In other words, it's not always true, but it always makes sense, it always has a truth value (when $a$ and $b$ have truth values). And the latter is what's needed for the defined expression $aland b$ to make sense.

share|cite|improve this answer

answered Sep 5 at 1:43

Andreas Blass

47.8k349106

I'm going to guess that you're conflating two different notions, namely "well-formed" and "logically valid". (My guess is admittedly based on just one little piece of one of your comments, namely "valid / makes sense".)

Of those two notions, only "well-formed" is relevant to definitions. You can define new symbols to abbreviate any well-formed formula, for example $neg(atoneg b)$. The well-formed formulas are the ones that "make sense", i.e., have a truth value once you specify truth values for the variables in them. For example (check this with a truth table if you haven't already done so), $neg(atoneg b)$ is true if both $a$ and $b$ are true, but $neg(atoneg b)$ is false in all other circumstances.

Of the two notions, only "logically valid" is governed by the axioms and inference rules. The axioms are certain, selected, logically valid formulas, and the inference rules enable us to produce additional logically valid formulas from the axioms. We'll never produce $neg(atoneg b)$ that way, because it's not logically valid. As indicated above, it's false sometimes (whenever at least one of $a$ and $b$ is false).

So $neg(atoneg b)$ is not valid, but it is well-formed. In other words, it's not always true, but it always makes sense, it always has a truth value (when $a$ and $b$ have truth values). And the latter is what's needed for the defined expression $aland b$ to make sense.

share|cite|improve this answer

answered Sep 5 at 1:43

Andreas Blass

47.8k349106

share|cite|improve this answer

share|cite|improve this answer

answered Sep 5 at 1:43

Andreas Blass

47.8k349106

answered Sep 5 at 1:43

Andreas Blass

47.8k349106

answered Sep 5 at 1:43

Andreas Blass

47.8k349106

47.8k349106

• 
  
  
  

  
  

  
  
  
  
  
  

  
  "Of those two notions, only "well-formed" is relevant to definitions." So, would you assert that if we defined (a$lor$b), where $lor$ gets understood as logical disjunction, as ¬(a→¬b) that would make sense as a definition? At the very least, that's different from conventional definitions, since conventional definitions usually preserve truth if you replace one side with another when one side appears as a subformula in some formula.
  – Doug Spoonwood
  Sep 5 at 3:20
  

  
  
  
  


• 
  
  
  

  
  

  
  
  
  
  
  

  
  @DougSpoonwood If we made that definition, we'd be introducing the symbol $lor$ to mean "and". Not a good idea, since people are accustomed to a different definition and are likely to be confused. But, in and of itself, it's a legitimate definition. (Note that people have used $sim$ to mean negation and other people have used the same symbol for biconditional. Either definition by itself is legitimate.)
  – Andreas Blass
  Sep 5 at 3:26
  

  
  
  
  


• 
  
  
  

  
  1
  

  
  
  
  
  
  

  
  @DougSpoonwood I should also say something about "where $lor$ gets understood as logical disjunction" in your comment. If we defined $lor$ in the way you described, then to understand $lor$ as logical disjunction would be to misunderstand it.
  – Andreas Blass
  Sep 5 at 3:29
  

  
  
  
  

add a comment | 

• 
  
  
  

  
  

  
  
  
  
  
  

  
  "Of those two notions, only "well-formed" is relevant to definitions." So, would you assert that if we defined (a$lor$b), where $lor$ gets understood as logical disjunction, as ¬(a→¬b) that would make sense as a definition? At the very least, that's different from conventional definitions, since conventional definitions usually preserve truth if you replace one side with another when one side appears as a subformula in some formula.
  – Doug Spoonwood
  Sep 5 at 3:20
  

  
  
  
  


• 
  
  
  

  
  

  
  
  
  
  
  

  
  @DougSpoonwood If we made that definition, we'd be introducing the symbol $lor$ to mean "and". Not a good idea, since people are accustomed to a different definition and are likely to be confused. But, in and of itself, it's a legitimate definition. (Note that people have used $sim$ to mean negation and other people have used the same symbol for biconditional. Either definition by itself is legitimate.)
  – Andreas Blass
  Sep 5 at 3:26
  

  
  
  
  


• 
  
  
  

  
  1
  

  
  
  
  
  
  

  
  @DougSpoonwood I should also say something about "where $lor$ gets understood as logical disjunction" in your comment. If we defined $lor$ in the way you described, then to understand $lor$ as logical disjunction would be to misunderstand it.
  – Andreas Blass
  Sep 5 at 3:29
  

  
  
  
  

"Of those two notions, only "well-formed" is relevant to definitions." So, would you assert that if we defined (a$lor$b), where $lor$ gets understood as logical disjunction, as ¬(a→¬b) that would make sense as a definition? At the very least, that's different from conventional definitions, since conventional definitions usually preserve truth if you replace one side with another when one side appears as a subformula in some formula.
– Doug Spoonwood
Sep 5 at 3:20

"Of those two notions, only "well-formed" is relevant to definitions." So, would you assert that if we defined (a$lor$b), where $lor$ gets understood as logical disjunction, as ¬(a→¬b) that would make sense as a definition? At the very least, that's different from conventional definitions, since conventional definitions usually preserve truth if you replace one side with another when one side appears as a subformula in some formula.
– Doug Spoonwood
Sep 5 at 3:20

@DougSpoonwood If we made that definition, we'd be introducing the symbol $lor$ to mean "and". Not a good idea, since people are accustomed to a different definition and are likely to be confused. But, in and of itself, it's a legitimate definition. (Note that people have used $sim$ to mean negation and other people have used the same symbol for biconditional. Either definition by itself is legitimate.)
– Andreas Blass
Sep 5 at 3:26

@DougSpoonwood If we made that definition, we'd be introducing the symbol $lor$ to mean "and". Not a good idea, since people are accustomed to a different definition and are likely to be confused. But, in and of itself, it's a legitimate definition. (Note that people have used $sim$ to mean negation and other people have used the same symbol for biconditional. Either definition by itself is legitimate.)
– Andreas Blass
Sep 5 at 3:26

1

1

@DougSpoonwood I should also say something about "where $lor$ gets understood as logical disjunction" in your comment. If we defined $lor$ in the way you described, then to understand $lor$ as logical disjunction would be to misunderstand it.
– Andreas Blass
Sep 5 at 3:29

@DougSpoonwood I should also say something about "where $lor$ gets understood as logical disjunction" in your comment. If we defined $lor$ in the way you described, then to understand $lor$ as logical disjunction would be to misunderstand it.
– Andreas Blass
Sep 5 at 3:29

add a comment | 

up vote
0
down vote

The key issue here is soundness.

The purpose of definitions in propositional calculus lies in converting notions not using the primitive connectives into well-formed formulas using only the primitive connectives, and doing the converse. In other words, definitions exist to translate between connectives.

There's an alternative way of expressing definitions by having a propositional calculus with functorial variables instead of a propositional calculus without functorial variables. Basically, it turns out that definitions which define connectives convert into tautologies with functorial variables of the form (in Polish notation)

C $delta$x $delta$y

where x is one-side of the definition, and y is the other-side of the definition. It also turns that if C $delta$x $delta$y, then Exy, and if Exy then C $delta$x $delta$y. Correspondingly, every definition has the property that one-side is logically equivalent to the other side of the definition. Thus, for any definition of a connective, if a well-formed formula gets written in Polish notation, the connective should appear once as the first symbol in the well-formed formula and only appear once in that well-formed formula. If some other formula equals it, then one can reasonably define that connective by that other formula.

For example, one common definition (again in Polish notation) is:

Apq := CNpq

which defines logical disjunction in terms of implication and negation. But, since

E Apq CCpqq

is a tautology also, and A appears the first symbol in 'Apq' and only appears once in 'Apq', one could use 'CCpqq' to define 'A' instead of using 'CNpq'.

To go over your questions one by one:

"Why is this permitted?"

Because anytime an instance of the formula (once parentheses get restored) on one side appears within a well-formed formula W, it can replace can get replaced by the formula (once parentheses get restored) on the right without W' changing from true to false, or from false to true. Or in short, definitional replacement preserves truth (this property is immediately evident for a formula like C $delta$x $delta$y once you understand how substitution for $delta$ works). Thus, it doesn't result in an invalidity. So, if the axioms are sound, definitional replacement preserves soundness.

"What are we allowed to define?"

Any connective can get defined in terms of formulas only having the primitive connectives of the system. This gets done to ensure that the system is adequate.

"What are we even using modus ponens and the axioms for if we can just make up whatever?"

Because only a subset or subclass of "whatever" will qualify as logically sound. Modus ponens is sound. So are the axioms. The definitions also either are sound, or work out as consistent with soundness. So again, the key issue here is soundness.

share|cite|improve this answer

answered Sep 5 at 3:15

Doug Spoonwood

7,82412043

add a comment | 

up vote
0
down vote

The key issue here is soundness.

The purpose of definitions in propositional calculus lies in converting notions not using the primitive connectives into well-formed formulas using only the primitive connectives, and doing the converse. In other words, definitions exist to translate between connectives.

There's an alternative way of expressing definitions by having a propositional calculus with functorial variables instead of a propositional calculus without functorial variables. Basically, it turns out that definitions which define connectives convert into tautologies with functorial variables of the form (in Polish notation)

C $delta$x $delta$y

where x is one-side of the definition, and y is the other-side of the definition. It also turns that if C $delta$x $delta$y, then Exy, and if Exy then C $delta$x $delta$y. Correspondingly, every definition has the property that one-side is logically equivalent to the other side of the definition. Thus, for any definition of a connective, if a well-formed formula gets written in Polish notation, the connective should appear once as the first symbol in the well-formed formula and only appear once in that well-formed formula. If some other formula equals it, then one can reasonably define that connective by that other formula.

For example, one common definition (again in Polish notation) is:

Apq := CNpq

which defines logical disjunction in terms of implication and negation. But, since

E Apq CCpqq

is a tautology also, and A appears the first symbol in 'Apq' and only appears once in 'Apq', one could use 'CCpqq' to define 'A' instead of using 'CNpq'.

To go over your questions one by one:

"Why is this permitted?"

Because anytime an instance of the formula (once parentheses get restored) on one side appears within a well-formed formula W, it can replace can get replaced by the formula (once parentheses get restored) on the right without W' changing from true to false, or from false to true. Or in short, definitional replacement preserves truth (this property is immediately evident for a formula like C $delta$x $delta$y once you understand how substitution for $delta$ works). Thus, it doesn't result in an invalidity. So, if the axioms are sound, definitional replacement preserves soundness.

"What are we allowed to define?"

Any connective can get defined in terms of formulas only having the primitive connectives of the system. This gets done to ensure that the system is adequate.

"What are we even using modus ponens and the axioms for if we can just make up whatever?"

Because only a subset or subclass of "whatever" will qualify as logically sound. Modus ponens is sound. So are the axioms. The definitions also either are sound, or work out as consistent with soundness. So again, the key issue here is soundness.

share|cite|improve this answer

answered Sep 5 at 3:15

Doug Spoonwood

7,82412043

add a comment | 

up vote
0
down vote

up vote
0
down vote

The key issue here is soundness.

The purpose of definitions in propositional calculus lies in converting notions not using the primitive connectives into well-formed formulas using only the primitive connectives, and doing the converse. In other words, definitions exist to translate between connectives.

There's an alternative way of expressing definitions by having a propositional calculus with functorial variables instead of a propositional calculus without functorial variables. Basically, it turns out that definitions which define connectives convert into tautologies with functorial variables of the form (in Polish notation)

C $delta$x $delta$y

where x is one-side of the definition, and y is the other-side of the definition. It also turns that if C $delta$x $delta$y, then Exy, and if Exy then C $delta$x $delta$y. Correspondingly, every definition has the property that one-side is logically equivalent to the other side of the definition. Thus, for any definition of a connective, if a well-formed formula gets written in Polish notation, the connective should appear once as the first symbol in the well-formed formula and only appear once in that well-formed formula. If some other formula equals it, then one can reasonably define that connective by that other formula.

For example, one common definition (again in Polish notation) is:

Apq := CNpq

which defines logical disjunction in terms of implication and negation. But, since

E Apq CCpqq

is a tautology also, and A appears the first symbol in 'Apq' and only appears once in 'Apq', one could use 'CCpqq' to define 'A' instead of using 'CNpq'.

To go over your questions one by one:

"Why is this permitted?"

Because anytime an instance of the formula (once parentheses get restored) on one side appears within a well-formed formula W, it can replace can get replaced by the formula (once parentheses get restored) on the right without W' changing from true to false, or from false to true. Or in short, definitional replacement preserves truth (this property is immediately evident for a formula like C $delta$x $delta$y once you understand how substitution for $delta$ works). Thus, it doesn't result in an invalidity. So, if the axioms are sound, definitional replacement preserves soundness.

"What are we allowed to define?"

Any connective can get defined in terms of formulas only having the primitive connectives of the system. This gets done to ensure that the system is adequate.

"What are we even using modus ponens and the axioms for if we can just make up whatever?"

Because only a subset or subclass of "whatever" will qualify as logically sound. Modus ponens is sound. So are the axioms. The definitions also either are sound, or work out as consistent with soundness. So again, the key issue here is soundness.

share|cite|improve this answer

answered Sep 5 at 3:15

Doug Spoonwood

7,82412043

The key issue here is soundness.

The purpose of definitions in propositional calculus lies in converting notions not using the primitive connectives into well-formed formulas using only the primitive connectives, and doing the converse. In other words, definitions exist to translate between connectives.

There's an alternative way of expressing definitions by having a propositional calculus with functorial variables instead of a propositional calculus without functorial variables. Basically, it turns out that definitions which define connectives convert into tautologies with functorial variables of the form (in Polish notation)

C $delta$x $delta$y

where x is one-side of the definition, and y is the other-side of the definition. It also turns that if C $delta$x $delta$y, then Exy, and if Exy then C $delta$x $delta$y. Correspondingly, every definition has the property that one-side is logically equivalent to the other side of the definition. Thus, for any definition of a connective, if a well-formed formula gets written in Polish notation, the connective should appear once as the first symbol in the well-formed formula and only appear once in that well-formed formula. If some other formula equals it, then one can reasonably define that connective by that other formula.

For example, one common definition (again in Polish notation) is:

Apq := CNpq

which defines logical disjunction in terms of implication and negation. But, since

E Apq CCpqq

is a tautology also, and A appears the first symbol in 'Apq' and only appears once in 'Apq', one could use 'CCpqq' to define 'A' instead of using 'CNpq'.

To go over your questions one by one:

"Why is this permitted?"

Because anytime an instance of the formula (once parentheses get restored) on one side appears within a well-formed formula W, it can replace can get replaced by the formula (once parentheses get restored) on the right without W' changing from true to false, or from false to true. Or in short, definitional replacement preserves truth (this property is immediately evident for a formula like C $delta$x $delta$y once you understand how substitution for $delta$ works). Thus, it doesn't result in an invalidity. So, if the axioms are sound, definitional replacement preserves soundness.

"What are we allowed to define?"

Any connective can get defined in terms of formulas only having the primitive connectives of the system. This gets done to ensure that the system is adequate.

"What are we even using modus ponens and the axioms for if we can just make up whatever?"

Because only a subset or subclass of "whatever" will qualify as logically sound. Modus ponens is sound. So are the axioms. The definitions also either are sound, or work out as consistent with soundness. So again, the key issue here is soundness.

share|cite|improve this answer

answered Sep 5 at 3:15

Doug Spoonwood

7,82412043

share|cite|improve this answer

share|cite|improve this answer

answered Sep 5 at 3:15

Doug Spoonwood

7,82412043

answered Sep 5 at 3:15

Doug Spoonwood

7,82412043

answered Sep 5 at 3:15

Doug Spoonwood

7,82412043

7,82412043

add a comment | 

add a comment | 

 

draft saved

draft discarded

 

draft saved

draft discarded

Sign up or log in

StackExchange.ready(function ()
StackExchange.helpers.onClickDraftSave('#login-link');
);

Sign up using Google

Sign up using Facebook

Sign up using Email and Password

Post as a guest

Name Email

StackExchange.ready(
function ()
StackExchange.openid.initPostLogin('.new-post-login', 'https%3a%2f%2fmath.stackexchange.com%2fquestions%2f2905685%2fdo-definitions-have-to-fit-axioms-in-logic%23new-answer', 'question_page');

);

Post as a guest

Name Email

Sign up or log in

StackExchange.ready(function ()
StackExchange.helpers.onClickDraftSave('#login-link');
);

Sign up using Google

Sign up using Facebook

Sign up using Email and Password

Post as a guest

Name Email

Sign up or log in

StackExchange.ready(function ()
StackExchange.helpers.onClickDraftSave('#login-link');
);

Sign up using Google

Sign up using Facebook

Sign up using Email and Password

Post as a guest

Name Email

Sign up or log in

StackExchange.ready(function ()
StackExchange.helpers.onClickDraftSave('#login-link');
);

Sign up using Google

Sign up using Facebook

Sign up using Email and Password

Sign up using Google

Sign up using Facebook

Sign up using Email and Password

Post as a guest

Name Email

Name Email

Name

Email

Name Email

Name

Email