“intuitionistic logic”的概念、定义、翻译、参考文献-科学参考

intuitionistic logic

Logic

Describes systems of propositional and first-order logic developed by Arend Heyting (1898–1980) as a formal axiomatization of the reasoning central to L. E. J. Brouwer’s (1881–1966) programme of intuitionism.
Given the Gödel-McKinsey-Tarski embedding of intuitionistic logic into $S 4$ , one can read intuitionistic logic as a scheme of reasoning in which assertion of a sentence $φ$ is the assertion of the provability of $φ$ . This makes many of the formal distinctions between intuitionistic and classical logic salient. For example, the double negation law:
- • $\neg\neg φ \to φ$
is rejected in intuitionistic logic. But to accept this scheme as a theorem is equivalent to the statement:
- • If one can prove that the rejection of $φ$ leads to absurdity, then one can prove $φ$ .
To assert, for example, that $\neg (φ \lor \neg φ)$ holds, i.e., that $(φ \lor \neg φ) \to ⊥$ , would entail that one could disprove both $φ$ and $\neg φ$ . But this is absurd from an intuitionistic perspective, hence $\neg (φ \lor \neg φ)$ leads to absurdity, or $\neg\neg (φ \lor \neg φ)$ . But the scheme:
- • $φ \lor \neg φ$
is also rejected, as it would entail that for any formula $φ$ , one has the means to either prove or disprove $φ$ .
This interpretation explains the failure of instances of one of De Morgan’s laws, i.e.:
- • $\neg (φ \land ψ) \to (\neg φ \lor \neg ψ)$
Should this scheme count as an axiom or theorem, then as an instance, one could infer in general that:
- • $\neg (φ \land \neg φ) \to (\neg φ \lor \neg\neg φ)$
Intuitionistic logic is not paraconsistent and one in general has a proof of the antecedent $\neg (φ \land \neg φ)$ of this formula; if $\neg φ$ is defined as the proof that $φ$ entails a contradiction, then as $φ \land \neg φ \to φ \land \neg φ, \neg (φ \land \neg φ)$ trivially follows. Accepting the consequent of this formula—known as weak excluded middle—as an axiom scheme would be to state that for any formula $φ$ , one has either a proof that $φ$ entails a contradiction or a proof that $φ$ can never entail a contradiction. But this is not true if $φ$ is, e.g., the Riemann Hypothesis.
Intuitionistic logic is a proper subsystem of classical logic and the addition of either the law of excluded middle ( $φ \lor \neg φ$ ) or Peirce’s law $((φ \to ψ) \to φ) \to φ$ as axiom schema generates classical logic.

Philosophy

The logical system developed initially by Arend Heyting (1898–1980) to formalize the reasonings allowed by mathematical intuitionism. It is designed so that p ∨¬p is not a theorem, and the rule of inference from ¬¬p to p is disallowed (the logic can be obtained from standard natural deduction treatments of the propositional calculus by dropping this rule, provided there is added a rule that from a contradiction anything follows). It should be noticed that intuitionism does not assert the negation of p ∨ ¬p. On the contrary, its double negation, ¬¬(p ∨ ¬p), is itself a theorem of intuitionistic logic. A further important property is that from ¬(∀x)Fx it cannot be shown that (∃x)¬Fx. This accords with the constructivist instincts behind intuitionism, since the premise gives us no way of constructing an instance of a thing that is not F. Gödel showed that intuitionistic logic can be mapped into the modal logic S4 by various translations of which this is an example. Here v is a propositional variable; A, B are any well-formed formulae of the intuitionistic logic, and Tr(a) is the translation of any formula into S4:
- Tr(v)=□v
- Tr(A v B)=TrA v TrB
- Tr(A & B)=TrA & TrB
- Tr(A → B)=TrA → TrB
- Tr ¬A=¬◊TrA.
This suggests that Heyting was guided by the thought that making a statement is equivalent to stating that the statement is provable or constructible. Denying a statement would be claiming that it is not possible that it should be constructed, or that a contradiction can be derived from the claim that it has been constructed. However, although these equivalences may help classical logicians to understand intuitionism, philosophically intuitionists would not accept that the classical modal logic is fundamental, or that such an explanation in classical terms is appropriate. An interesting property of intuitionistic logic is that no finite truth tables can be given for the connectives.

单词	intuitionistic logic
释义	intuitionistic logic Logic Describes systems of propositional and first-order logic developed by Arend Heyting (1898–1980) as a formal axiomatization of the reasoning central to L. E. J. Brouwer’s (1881–1966) programme of intuitionism. Given the Gödel-McKinsey-Tarski embedding of intuitionistic logic into $S 4$ , one can read intuitionistic logic as a scheme of reasoning in which assertion of a sentence $φ$ is the assertion of the provability of $φ$ . This makes many of the formal distinctions between intuitionistic and classical logic salient. For example, the double negation law: • $\neg\neg φ \to φ$ is rejected in intuitionistic logic. But to accept this scheme as a theorem is equivalent to the statement: • If one can prove that the rejection of $φ$ leads to absurdity, then one can prove $φ$ . To assert, for example, that $\neg (φ \lor \neg φ)$ holds, i.e., that $(φ \lor \neg φ) \to ⊥$ , would entail that one could disprove both $φ$ and $\neg φ$ . But this is absurd from an intuitionistic perspective, hence $\neg (φ \lor \neg φ)$ leads to absurdity, or $\neg\neg (φ \lor \neg φ)$ . But the scheme: • $φ \lor \neg φ$ is also rejected, as it would entail that for any formula $φ$ , one has the means to either prove or disprove $φ$ . This interpretation explains the failure of instances of one of De Morgan’s laws, i.e.: • $\neg (φ \land ψ) \to (\neg φ \lor \neg ψ)$ Should this scheme count as an axiom or theorem, then as an instance, one could infer in general that: • $\neg (φ \land \neg φ) \to (\neg φ \lor \neg\neg φ)$ Intuitionistic logic is not paraconsistent and one in general has a proof of the antecedent $\neg (φ \land \neg φ)$ of this formula; if $\neg φ$ is defined as the proof that $φ$ entails a contradiction, then as $φ \land \neg φ \to φ \land \neg φ, \neg (φ \land \neg φ)$ trivially follows. Accepting the consequent of this formula—known as weak excluded middle—as an axiom scheme would be to state that for any formula $φ$ , one has either a proof that $φ$ entails a contradiction or a proof that $φ$ can never entail a contradiction. But this is not true if $φ$ is, e.g., the Riemann Hypothesis. Intuitionistic logic is a proper subsystem of classical logic and the addition of either the law of excluded middle ( $φ \lor \neg φ$ ) or Peirce’s law $((φ \to ψ) \to φ) \to φ$ as axiom schema generates classical logic. Philosophy The logical system developed initially by Arend Heyting (1898–1980) to formalize the reasonings allowed by mathematical intuitionism. It is designed so that p ∨¬p is not a theorem, and the rule of inference from ¬¬p to p is disallowed (the logic can be obtained from standard natural deduction treatments of the propositional calculus by dropping this rule, provided there is added a rule that from a contradiction anything follows). It should be noticed that intuitionism does not assert the negation of p ∨ ¬p. On the contrary, its double negation, ¬¬(p ∨ ¬p), is itself a theorem of intuitionistic logic. A further important property is that from ¬(∀x)Fx it cannot be shown that (∃x)¬Fx. This accords with the constructivist instincts behind intuitionism, since the premise gives us no way of constructing an instance of a thing that is not F. Gödel showed that intuitionistic logic can be mapped into the modal logic S4 by various translations of which this is an example. Here v is a propositional variable; A, B are any well-formed formulae of the intuitionistic logic, and Tr(a) is the translation of any formula into S4: Tr(v)=□v Tr(A v B)=TrA v TrB Tr(A & B)=TrA & TrB Tr(A → B)=TrA → TrB Tr ¬A=¬◊TrA. This suggests that Heyting was guided by the thought that making a statement is equivalent to stating that the statement is provable or constructible. Denying a statement would be claiming that it is not possible that it should be constructed, or that a contradiction can be derived from the claim that it has been constructed. However, although these equivalences may help classical logicians to understand intuitionism, philosophically intuitionists would not accept that the classical modal logic is fundamental, or that such an explanation in classical terms is appropriate. An interesting property of intuitionistic logic is that no finite truth tables can be given for the connectives.
随便看	Pico della Mirandola, Giovanni (1463–94) picoplankton picornavirus picosatellite Picosatellite for Remote-sensing and Innovative Space Missions pico-(symbol: p) Pico Veleta picrate picric acid picrite PICT Pict Pictet, Raoul Pierre pictogram Pictor picture picture carrier picture element picture processing picture theory of meaning P&ID PID PID control PID controller Pidgeon process