more on this theme
|
more from this thinker
Single Idea 13690
[filed under theme 5. Theory of Logic / H. Proof Systems / 3. Proof from Assumptions
]
Full Idea
The style of proof called 'induction on formula construction' (or 'on the number of connectives', or 'on the length of the formula') rest on the fact that all formulas are built up from atomic formulas according to strict rules.
Gist of Idea
Proof by induction 'on the length of the formula' deconstructs a formula into its accepted atoms
Source
Theodore Sider (Logic for Philosophy [2010], 2.7)
Book Ref
Sider,Theodore: 'Logic for Philosophy' [OUP 2010], p.52
A Reaction
Hence the proof deconstructs the formula, and takes it back to a set of atomic formulas have already been established.
The
45 ideas
from 'Logic for Philosophy'
13678
|
The most popular account of logical consequence is the semantic or model-theoretic one
[Sider]
|
13682
|
Maybe logical consequence is impossibility of the premises being true and the consequent false
[Sider]
|
13680
|
Maybe logical consequence is a primitive notion
[Sider]
|
13679
|
Maybe logical consequence is more a matter of provability than of truth-preservation
[Sider]
|
13683
|
A relation is a feature of multiple objects taken together
[Sider]
|
13724
|
In model theory, first define truth, then validity as truth in all models, and consequence as truth-preservation
[Sider]
|
13684
|
The semantical notion of a logical truth is validity, being true in all interpretations
[Sider]
|
13685
|
Natural deduction helpfully allows reasoning with assumptions
[Sider]
|
13686
|
We can build proofs just from conclusions, rather than from plain formulae
[Sider]
|
13688
|
Good axioms should be indisputable logical truths
[Sider]
|
13687
|
No assumptions in axiomatic proofs, so no conditional proof or reductio
[Sider]
|
13689
|
'Theorems' are formulas provable from no premises at all
[Sider]
|
13691
|
Induction has a 'base case', then an 'inductive hypothesis', and then the 'inductive step'
[Sider]
|
13690
|
Proof by induction 'on the length of the formula' deconstructs a formula into its accepted atoms
[Sider]
|
13692
|
A 'precisification' of a trivalent interpretation reduces it to a bivalent interpretation
[Sider]
|
13693
|
A 'supervaluation' assigns further Ts and Fs, if they have been assigned in every precisification
[Sider]
|
13695
|
Supervaluational logic is classical, except when it adds the 'Definitely' operator
[Sider]
|
13694
|
We can 'sharpen' vague terms, and then define truth as true-on-all-sharpenings
[Sider]
|
13697
|
Valuations in PC assign truth values to formulas relative to variable assignments
[Sider]
|
13696
|
When a variable is 'free' of the quantifier, the result seems incapable of truth or falsity
[Sider]
|
13698
|
In a complete logic you can avoid axiomatic proofs, by using models to show consequences
[Sider]
|
13699
|
Compactness surprisingly says that no contradictions can emerge when the set goes infinite
[Sider]
|
13700
|
A 'total' function must always produce an output for a given domain
[Sider]
|
13701
|
A single second-order sentence validates all of arithmetic - but this can't be proved axiomatically
[Sider]
|
13702
|
The identity of indiscernibles is necessarily true, if being a member of some set counts as a property
[Sider]
|
13703
|
λ can treat 'is cold and hungry' as a single predicate
[Sider]
|
13705
|
Truth tables assume truth functionality, and are just pictures of truth functions
[Sider]
|
13704
|
It is hard to say which are the logical truths in modal logic, especially for iterated modal operators
[Sider]
|
13706
|
Intuitively, deontic accessibility seems not to be reflexive, but to be serial
[Sider]
|
13707
|
Maybe metaphysical accessibility is intransitive, if a world in which I am a frog is impossible
[Sider]
|
13708
|
S5 is the strongest system, since it has the most valid formulas, because it is easy to be S5-valid
[Sider]
|
13709
|
Logical truths must be necessary if anything is
[Sider]
|
13710
|
In D we add that 'what is necessary is possible'; then tautologies are possible, and contradictions not necessary
[Sider]
|
13711
|
System B introduces iterated modalities
[Sider]
|
13712
|
Epistemic accessibility is reflexive, and allows positive and negative introspection (KK and K¬K)
[Sider]
|
13714
|
We can treat modal worlds as different times
[Sider]
|
13715
|
You can employ intuitionist logic without intuitionism about mathematics
[Sider]
|
13716
|
'If B hadn't shot L someone else would have' if false; 'If B didn't shoot L, someone else did' is true
[Sider]
|
13717
|
Transworld identity is not a problem in de dicto sentences, which needn't identify an individual
[Sider]
|
13719
|
Barcan Formula problem: there might have been a ghost, despite nothing existing which could be a ghost
[Sider]
|
13720
|
Converse Barcan Formula: □∀αφ→∀α□φ
[Sider]
|
13718
|
The Barcan Formula ∀x□Fx→□∀xFx may be a defect in modal logic
[Sider]
|
13721
|
'Strong' necessity in all possible worlds; 'weak' necessity in the worlds where the relevant objects exist
[Sider]
|
13723
|
System B is needed to prove the Barcan Formula
[Sider]
|
13722
|
A 'theorem' is an axiom, or the last line of a legitimate proof
[Sider]
|