≡ formal system of logic ≡ logic system
≡ mathematical logic ≡ logistic ≡ symbolic logic (historically called) ≡ algebra of logic ≡ formal logic (more recently)
Consists of a
what is logic still remains one of the main subjects of research and debates in the field of philosophy of logic.
Anche l'attuale (2020) descrizione su wikipedia e' un po' sparpagliata.
Un buon punto di partenza e'
Combinatory_logic | stanford/logic-combinatory
per comprendere, un minimo di storia.
goes from premises to conclusions. If all premises are true, and the rules of deductive logic are followed, then the conclusion reached is necessarily true.
en: Logical_consequence, entailment, implication;
fr: Déduction logique;
es: Consecuencia lógica
wp/Logic#Inference | wp/Inference
Occa: ho sempre detto per "se X allora Y" "X implica Y", ma secondo l'articolo la relazione tra i 2 e' piu' complessa.
the logician traditionally is not interested in the sentence as uttered but in the proposition, an idealised sentence suitable for logical manipulation.
proposition_(mathematics) a statement that is true or not true;
axiom a statement that is taken to be true within a domain of discourse.
Frase dichiarativa (affermazione), interrogativa
An interpretation is an assignment of meaning to the symbols of a formal language.
Many formal languages used in mathematics, logic, and theoretical computer science are defined in solely syntactic terms, and as such do not have any meaning until they are given some interpretation.
formal semantics (=def) the general study of interpretations of formal languages
ref: Interpretation_(logic) | Semantics_of_logic formal semantics
formal system wp
is an abstract structure used for inferring theorems from axioms according to a set of rules.
These rules, which are used for carrying out the inference of theorems from axioms, are the logical calculus of the formal system.
A formal system is essentially an "axiomatic system".
In 1921, David Hilbert proposed to use such a system as the foundation for the knowledge in mathematics.
The logician is concerned with
So an handy notation
“Γ ⊢ A” means: Γ is a set of axioms, A is a particular proposition
Often the Γ is omitted when the discussion is in context of a particular set of axioms and then “⊢ A” means that A may be deduced from those axioms, i.e. that A is a theorem in the formal system. Sometimes more than one set of deduction rules are under discussion and then there will be a subscript to the turnstile.
The simplest and most common deduction rule is merely modus ponens.