Syntax
Language
The language of the propositional logic BL consists of countably many propositional variables and the following primitive logical connectives:
- Implication (binary) (binary)
- Strong conjunction (binary). The sign & is a more traditional notation for strong conjunction in the literature on fuzzy logic, while the notation (binary). The sign & is a more traditional notation for strong conjunction in the literature on fuzzy logic, while the notation follows the tradition of substructural logics. follows the tradition of substructural logics.
- Bottom (nullary — a propositional constant); (nullary — a propositional constant); or or are common alternative signs and zero a common alternative name for the propositional constant (as the constants bottom and zero of substructural logics coincide in MTL). are common alternative signs and zero a common alternative name for the propositional constant (as the constants bottom and zero of substructural logics coincide in MTL).
The following are the most common defined logical connectives:
- Weak conjunction (binary), also called lattice conjunction (as it is always realized by the lattice operation of meet in algebraic semantics). Unlike MTL and weaker substructural logics, weak conjunction is definable in BL as (binary), also called lattice conjunction (as it is always realized by the lattice operation of meet in algebraic semantics). Unlike MTL and weaker substructural logics, weak conjunction is definable in BL as
 
 
- Negation (unary), defined as (unary), defined as
 
 
- Equivalence (binary), defined as (binary), defined as
 
 
- As in MTL, the definition is equivalent to  
- (Weak) disjunction (binary), also called lattice disjunction (as it is always realized by the lattice operation of join in algebraic semantics), defined as (binary), also called lattice disjunction (as it is always realized by the lattice operation of join in algebraic semantics), defined as
 
 
- Top (nullary), also called one and denoted by (nullary), also called one and denoted by or or (as the constants top and zero of substructural logics coincide in MTL), defined as (as the constants top and zero of substructural logics coincide in MTL), defined as
 
 
 Well-formed formulae of BL are defined as usual in propositional logics. In order to save parentheses, it is common to use the following order of precedence:
- Unary connectives (bind most closely)
- Binary connectives other than implication and equivalence
- Implication and equivalence (bind most loosely)
Axioms
A Hilbert-style deduction system for BL has been introduced by Petr Hájek (1998). Its single derivation rule is modus ponens:
- from  and and derive derive 
The following are its axiom schemata:
 
The axioms (BL2) and (BL3) of the original axiomatic system were shown to be redundant (Chvalovský, 2012) and (Cintula, 2005). All the other axioms were shown to be independent (Chvalovský, 2012).
This page is based on this 
Wikipedia article Text is available under the 
CC BY-SA 4.0 license; additional terms may apply.
Images, videos and audio are available under their respective licenses.