-
Notifications
You must be signed in to change notification settings - Fork 1
Language
Grammar, terminology, and semantics all come from the book "Meaning and Argument: An Introduction To Logic Through Language", with some exceptions, but it is made clear (hopefully) throughout this page which ones these are. I try to introduce as little new grammar or terminology to the book as possible, but there are certain fundamental terms behind what is explained that are not so well-defined or obvious to the reader; most of the definitions I added (for tokens, types, well-formed formulas, bound/unbound predicates) is likely less 'general' (and maybe even flat-out wrong!) than what someone more knowledgeable of logic might come up with, but it does the job (they're internal to the language). Semantics are for the most part not discussed here since they are not modified from this book and are not specific to it either (I suppose?). Unicode tokens, like the book uses, are used.
A formal specification of the grammar can be found here. This specification, however, cannot account for a few context-sensitive details of the language (making sure degree of predicate matches number of terms, disallowing binding variable that's already in use to some quantifier, disallowing predicate binding to variable that isn't in scope), so here are documented, in English, all the rules adopted from the book that are necessary to write the interpreter and write valid RPL formulas.
The following rules are based off the book but not fully from it:
-
A token is any occurrence of a type.
-
A type is any instantiation of a well-formed expression.
-
A well-formed expression is any character or string of characters with a well-defined meaning, e.g. a statement or a connective (ANYTHING that has any grammatical meaning is an expression).
-
The instantiation of a symbol is the symbol itself.
-
A compound formula is any formula which connects atomic formulas via the logical connectives below.
-
Groupers are used to specify precedence/scope. They are symbolized by the tokens '(' (opening) and ')' (closing), and some expression sits in between them. There can be as many levels of groupers as required.
-
White spaces/return are allowed between any token, except in between component tokens of atomic formulas or terms.
-
A statement set is delimited by curly brackets: '{' (opening) and '}' (closing). Between each bracket, there can be one or more statements separated by a comma ','.
-
An argument is composed of one or more premises (which are statements), each separated from the other by a comma ',', and one conclusion (also a statement), indicated by the token '∴' (therefore). The conclusion must follow after the premises. There is no comma between the last premise and the conclusion.
-
A simple statement is a kind of statement which is symbolized by a single capital block letter from the alphabet ('A', 'B', 'C', 'D',...,'Z'), with the option of adding a subscript to them, as in 'A1', 'A2',...,'An' (only positive integers are allowed as subscripts; leading zeros are not allowed). Each different combination of letter/subscript is an instantiation of a simple statement, and thus a single token. If multiple tokens of the same combination appear, it is assumed that it is meant to be the same type. Parentheses are optional around a token of a simple statement.
-
A logical conjunction is a kind of statement which is symbolized by the connective '&' (the ampersand). It takes two conjuncts, one on each side of the symbol, which must both be statements. That is, if α and β are statements, then so is '(α & β)'. Parentheses are required around a logical conjunction.
-
A logical negation is a kind of statement which is symbolized by the connective '~' (the tilde). It takes one conjunct, at the right of the symbol, which must be a statement. That is, if α is a statement, then so is '~α'. Parentheses are optional around a logical negation.
-
A logical disjunction is a kind of statement which is symbolized by the connective '∨' (the vel; kind of incorrectly called wedge throughout the book?). It takes two conjuncts, one on each side of the symbol, which must both be statements. That is, if α and β are statements, then so is '(α ∨ β)'. Parentheses are required around a logical disjunction.
-
A logical conditional is a kind of statement which is symbolized by the connective '⊃' (the horseshoe). It takes two conjuncts, one on each side of the symbol, which must both be statements. That is, if α and β are statements, then so is '(α ⊃ β)'. Parentheses are required around a logical conditional.
-
A statement can have only one main connective (a main connective is such connective that has the widest scope in the statement; connectives are the tokens of symbols that represent each complex statement). In the book, an exception is made to the use of groupers where the resulting expression is unambiguous. Here, I will only allow parentheses to be omitted when there is no possibility of ambiguity. Unfortunately, unlike in the book, I can't allow groupers sometimes and not allow groupers some other times. I either enforce groupers, or make them optional everywhere and implement operator precendence. Since the goal is to stay as true to the book's grammar as possible, I opted for the former.
-
Only logical conjunctions, logical negations, logical disjunctions, and logical conditionals are complex statements.
-
Only simple and complex statements are well-formed formulas. Only complex statements are compound formulas, and only simple statements are atomic formulas.
-
Only simple and complex statements are statements.
-
A singular term is symbolized by a single lower case letter from the alphabet ('a', 'b', 'c',...,'w'). As with statement letters (the symbolization of a simple statement), singular terms can be subscripted as well, as in 'a1'. 'x', 'y', and 'z' are reserved for use as variables in RPL. Each different combination of letter/subscript is an instantiation of a singular term. If multiple tokens of the same combination appear, it is assumed that it is meant to be the same type.
-
Singular terms are terms.
-
Property predicates are symbolized by capital letters superscripted with the numeral '1' (the degree of the predicate), as in 'A1', 'B1', 'C1',...,'Z1'. These can also be subscripted, as in 'A11', 'A21', 'Bn1'. Each different combination of letter/subscript with degree one is an instantiation of a property predicate, and thus a single token. If multiple tokens of the same combination appear, it is assumed that it is meant to be the same type. Parentheses are optional around property predicates.
-
Property predicates can be followed by a single token of a singular term type, without any spaces between them, as in 'A1b', where 'A1' is a property predicate and 'b' is a token of a singular term type, forming singular subject-predicate statements. Such expressions are atomic formulas.
-
Singular subject-predicate statements are a kind of simple statement. Because they are a kind of simple statement, the rule of optional parentheses around them also applies.
-
Predicates can be either simple or compound. A simple predicate is simply a property predicate. A compound predicate is composed of other predicates joined together by one or more of the four connectives from PL: '&', '~', '∨', and '⊃', as in '(P1 & M1)'. Because the four connectives from PL only worked with statements, it begs for 7.
-
The four connectives from PL ('&', '~', '∨', and '⊃') can take left and right conjunctions of any statement or predicate type. When both left and right conjuncts are statements, the resulting formula is a statement. When both left and right conjuncts are predicates, the resulting formula is a compound predicate.
-
Both simple predicates and compound predicates are well-formed formulas. Simple predicates are atomic formulas, while compound predicates are compound formulas.
-
An existential quantifier statement is a kind of statement which is symbolized by the symbol '∃' (backwards 'E'), followed by a formula, either atomic or compound. Parentheses are optional around the quantifier + variable, as in '(∃x)', although not '(∃)x' or '∃(x)'.
-
An universal quantifier statement is a kind of statement which is symbolized by the symbol '∀' (upside-down 'A'), followed by a formula, either atomic or compound. Parentheses are optional around the quantifier + variable, as in '(∀x)', although not '(∀)x' or '∀(x)'.
-
Both existential and universal quantifier statements are kinds of complex statements.
-
Simple predicates, namely property predicates, are extended to work with any degree >=1. They are symbolized as 'An', 'Bn', and so on, where 'n' is the degree of the predicate, which denotes the number of terms attached - it must always coincide with the number of terms attached. All other rules still apply (namely, rule 4 and rule 3 from PPL grammar with the exceptions from here). Each different combination of letter/subscript/degree is an instantiation of a different simple predicate type. Simple predicates can be bound or unbound. If they're bound, they form a statement (all terms are singular terms). If they're not, then they have at least one place that is bound to a variable. Bound predicates are atomic formulas, and also singular statements (by the rule 4 from PPL).
-
The set of tokens of terms that appear attached to simple predicates is always interpreted in the same order.
-
A variable is symbolized by a single lower case letter from 'x' to 'z', and can be subscripted as well, as in 'x1', 'y2', etc.
-
Variables are terms.
-
Quantifiers must always bind to a variable.
-
A variable that is already bound to a quantifier cannot be bound to another quantifier in the same scope, for example, where there are nested quantifiers.
This is the syntax for RPL for now.
- The input can only be either a statement set, an argument, or a single statement.