Is "discharging assumptions" a deliberate, separate act or do we simply close a subdeduction?
Assumption is not an assertive act. Assumption is a directive act and that is why it is performed using an imperative sentence, "Assume/ suppose/ let ...!". "Discharging assumption" is a separate act of returning to the assertive mode.
@ John Cororan
I would hardly call your suppositional rules ordinary reasoning. Those are the contrivances of a formal deductive system. But in any case, the ideas of assumption discharge and subdeduction are peculiar to certain ways of setting up or displaying your proof procedures and can in principle be dispensed with.
In a sequent-style system every sequent can stand on its own; no sequent has a peculiar compromised status that segregates it from other sequents. One can still talk the talk (in the metalanguage) of "undischarged assumptions" or "propositions within a subdeduction" with regard to proof strategies, but they need not be structured as such on the page. Or, to put it in @Berislav Žarnić 's terms, directive and assertive modes need not be represented differently in the notation of the object language.
- Badges
- Science topic
- Similar topics
- Philosophy
- Philosophy Of Science
- Reasoning