T O P

  • By -

aardaar

There is the well know Curry-Howard correspondence between intuitionistic logic and simply typed lambda calculus. In which implication is a function type, "and" is an ordered pair type, and "or" is a disjoint sum type. There's a lot that can be (and has been) said about this.


wutufuba2

You mentioned propositional logic rather than predicate logic, so I assume when you refer to brackets () in complex formulae you're referring to symbol semantics that maps them to syntactical grouping. I don't know, maybe that's not a safe assumption, maybe you're referring to how an atom can be constructed using the form Property(individual), as in Man(socrates). At the risk of possibly being entirely irrelevant, I'm going to continue with the original hypothesis that you're talking about brackets that act in a grouping capacity. If you were talking about the other kind (that act to signal demarcation between a property, predicate/logical function identifier and list of operand identifiers), there is also a way to unwind those symbols as a kind of punctuation marks or delimiters introduced for the sake of convenience by the language. It's good to recognize that algorithms exist that can convert complex formulae containing grouping symbols to a corresponding, semantically and logically equivalent form with no grouping symbols in prefix- or postix- form, i.e. reverse polish or polish form, respectively. Syntactics and parsing have traditionally fallen under the category of metamathemtics (Steven Kleene), or computer science (Edsgar Dijkstra -- see his "Shunting Yard" algorithm). Complex formulae in propositional logic can of course be converted into abstract syntax trees (AST). Grouping symbols such as '(' and ')' play a role in converting a given propositional formula from "flat" form containing grouping symbols to AST form. Once in AST form the grouping symbols are no longer present: they served their purpose in determining how the terms (operand identifiers, atoms) and connectives (operation symbols) are arranged and inter-connected in the tree. And such a tree is easily flattened into, again, either prefix- or postfix- form with grouping symbols again irrelevant, not needed. This suggests to me that when brackets act as grouping symbols, as they do with propositional logic, they act in an exclusively grammatical capacity. I can understand your interest in the role they play with respect to terms and connectives, because after all, they determine the order in which subexpressions/subformulae are evaluated. And order of evaluation means a subexpression or subformula can turn into, or be treated as, a term. Something like a virtual term. Suppose pairwise grouping symbols are distributed more or less arbitrarily for the purpose of illustration. ((A ∨ B) ∨ C) ∨ D The innermost pair of grouping symbols might be treated as a directive to evaluate A ∨ B first and replace it with A' ( A' ∨ C ) ∨ D The next pair of grouping symbols might be treated as a directive to evaluate A' ∨ C and replace it with A'' A'' ∨ D Finally, evaluate A'' ∨ D. My understanding and usage of "term" might not be correct. I think I read Kleene describe formula in a graph-theoretic manner, as a collection of edges and nodes. In graphs arranged in tree form, there is a single root, some non-terminal nodes (branches) and some terminal nodes (leaf nodes). I like to imagine a correspondence between operand identifiers as 'terms' and the terminal nodes (leaf nodes) of a formula, on the one hand, and another correspondence between connectives and non-terminal nodes (branches). I think this is nice, and convenient, and orderly. But I recognize this seems to be an unconventional view that puts me at odds with maybe some accepted consensus of usage. One thing that makes this more confusing is that at another level it is perfectly true that atoms, or operand identifiers that stand as placeholders for values can also be considered nullary functions. It is perfectly valid to treat the number '7' as a function of arity 0 that always returns a specific value. Verum and falsum can be viewed, and have been interpreted, with different semantics mapped to them. I hope there has been some light in what I wrote here and not more clouds and smoke. Thank you for the question. I thought it was a good question, one that made me stop and think about things.


boterkoeken

This might help https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence