Prawitz’s semantics and Walton’s argument schemes: a tentative reading and application of Kreisel’s informal rigour
Résumés
Nous proposons une interprétation de la rigueur informelle de Kreisel comme interaction entre niveau formel et niveau informel dans l’analyse de concepts logiques fondamentaux. Pour étayer cette interprétation, nous considérons deux cas d’étude : la sémantique de Prawitz et l’analyse des schémas argumentaux de Walton. La sémantique de Prawitz suggère une interaction entre des présupposés informels, confirmés et affinés par des résultats formels, et des configurations formelles, qui peuvent être renforcées à travers une formalisation adéquate des présupposés informels. Dans la théorie de l’argumentation de Walton, les schémas argumentaux décrivent des arguments qui prouvent leur conclusion de manière présomptive. Cela peut être développé à travers des instruments formels utilisés en IA, ce qui montre l’importance de l’interaction entre ces deux niveaux dans l’analyse de la défectibilité.
Entrées d’index
Haut de pagePlan
Haut de pageTexte intégral
1. Introduction
 1 ^{ }G. Crocco, “Informal and absolute proofs: some remarks from a Gödelian perspective”, in G. Crocco (...)
1Philosophy of mathematical practice usually conceives of Kreisel’s informal rigour as a conceptual basis for the idea that one should abandon the socalled standard view of proofs and adopt an informal approach to mathematical reasoning. Building upon an interpretative line first proposed by Crocco,1 we here adopt a quite different reading. We argue that Kreisel’s aim is not to deny the importance of the formalistic moment, but rather to hint at a dialectic interaction between the intuitive and the formal level. The analysis of the intuitive notions allows for the development of more and more accurate formal setups and, vice versa, the improvement of these setups permits a better understanding of the informal concepts. The interpretation of Kreisel’s informal rigour we choose to adopt, if acceptable, would thus permit a seemingly new perspective for reflecting upon the relation between the formal and the informal moment, i.e. these moments are not opposite, but complementary. To substantiate our claim we investigate two casestudies: Prawitz’s semantics and Walton’s analysis of argument schemes.
2. A reading of Kreisel’s informal rigour
 2 ^{ }G. Kreisel, “Informal rigour and completeness proofs”, in I. Lakatos (ed.), Problems in the philo (...)
 3 ^{ }G. Kreisel, “Ordinal logics and the characterization of informal concepts of proof”, in J. A. Tod (...)
2In what follows, we refer to Kreisel’s wellknown Informal rigour and completeness proofs.2 Of course, other papers from Kreisel may be relevant, but we will leave them aside here.3 In 1967 Kreisel starts from formal rigour, and states that it
 4 ^{ }G. Kreisel, “Informal rigour and completeness proofs”, art. cit., p. 138.
consists in setting out formal rules and checking that a given derivation follows these rules [… it] does not apply to the discovery or choice of formal rules nor of notions.4
3In contrast to this, we have informal rigour, i.e.
 5 ^{ }Id., p. 138.
the old fashioned idea [that] one obtains rules and definitions by analysing intuitive notions and putting down their properties. […] intuitive notions are significant, be it in the external world or in thought.5
 6 ^{ }Id., p. 138.
4Informal rigour splits into two activities: (1) analysing intuitive notions in an as precise as possible way, so as to eliminate doubtful properties of these notions, and (2) extending this analysis by highlighting properties of the intuitive notions, so as to get rid of certain undecided questions. The analysis is carried out “with the means available”,6 so it is based on formal setups that account for the intuitive notions. The undecided questions clarified by extending the analysis may accordingly concern both the intuitive notions, and the formal setups inspired by them.
 7 ^{ }N. Barton, “Structural relativity and informal rigour”, in G. Oliveri, S. Boscolo and C. Ternullo (...)
5To give a schematic account of Kreisel’s informal rigour (partially in line with the one provided by Barton),7 we may thus say that it seemingly involves at least the following ingredients:

intuitive notions which we aim at exploring  set, consequence, and so on;

formal setups, possibly inspired by intuitive notions  nth order logic or settheory, ZFC plus additional axioms, and so on;

formal results concerning formal setups, possibly permitting to establish a connection between these setups  completeness, incompleteness or independence results, isomorphisms or categoricity of theories, and so on;

informal results obtained by reflecting upon the relation between formal setups and the intuitive notions underlying them.
6Point d) is the least precise, but eventually the most fruitful. Examples may be Kreisel’s socalled “squeezing argument”, arguments for and against the ChurchTuring thesis, formal results out of Brouwer’s philosophical standpoint and –as we shall argue below– Gentzen’s claim that his natural deduction rules may be considered as providing a semantic insight.
7Informal rigour is the activity that permits us to bridge these ingredients, and thereby obtain insights which would be unattainable if we stayed within the formal setups only. On the other hand, however, these insights must be obtained, as said, “with the means available”, that is, they depend on how formal setups are made, and on the formal or informal results we can prove within or about them. Thus, the scope of informal rigour is broad and hardly regimentable, but some examples of what it permits to do may be:

building formal setups out of intuitive notions by which these setups are inspired;

if some such setups are already available, formal or informal results concerning them may be used for developing the others;

seeking connections and extensions of these setups, based on properties of the intuitive notions underlying them, or on formal or informal results concerning them;

connections and extensions may be based on previously unaddressed properties of the intuitive notions, thus leading to a sharpening of these notions and of their relation with the corresponding formalisation.
8Therefore, informal rigour might be a neverending process. Starting from formal configurations and from formal or informal results within and about them, informal rigour yields new results relative to the formal configurations and to their relation with the intuitive notions. Or it highlights new properties of the intuitive notions. Given these new results and properties, new informally rigorous steps become possible.
 8 ^{ }For this see e.g. M. Antonutti Marfori, “Informal proofs and mathematical rigor”, Studia Logica, (...)
 9 ^{ }A defence of this interpretation can be found in G. Crocco, “Informal and absolute proofs…”, art. (...)
9If our reconstruction is acceptable, informal rigour could be understood as a continuous, dialectic interaction between the formal and the intuitive level. Under this reading, it should not be understood as opposed to the socalled standard view of proofs,8 but as complementary with it.9 We now propose two casestudies inspired by this claim, with the aim of rendering more plausible the claim itself, and of hinting at some interesting consequences of it.
3. Prawitz’s semantics
 10 ^{ }For the semantics of valid arguments we mainly refer to D. Prawitz, “Towards a foundation of gene (...)
10In this section we briefly outline Prawitz’s semantics, which comes in basically two forms: semantics of valid argument (SVA) and theory of grounds (ToG).10 Then, we highlight some presuppositions and structural properties of both SVA and ToG.
3.1. Valid arguments and grounds
11SVA is based on the notion of valid argument, which in turn requires three ingredients. First, atomic bases, namely, triples ⟨𝙲, 𝚁, 𝚂⟩ where 𝙲 and 𝚁 are, respectively, the set of the individual and of the predicate constants of a background language 𝐿, and 𝚂 is an atomic system over a sublanguage of 𝐿. Second, argument skeletons ∆, namely, formulas of 𝐿 arranged in a treeform of arbitrary inferences
 11 ^{ }G. Gentzen, “Untersuchungen über das logische schließen”, Matematische Zeitschrift, vol. 39, 1934 (...)
12for any 𝐴_{1}, …, 𝐴_{n}, 𝐵. Some inferences may bind individual variables and assumptions. ∆ is in canonical form if the last inference is a gentzenian introduction,11 otherwise it is in noncanonical form. ∆ is closed if it contains no unbound variables or undischarged assumptions, otherwise it is open. And finally we have constructive procedures 𝔍 for nonintroductory inferences, namely, total constructive functions from and to argument skeletons –whose output is a skeleton with the same conclusion as the skeleton to which the procedure is applied, and no unbound variables or assumptions not already occurring in this skeleton. Procedures are meant to “justify” inferences by showing how applications of them to “acceptable” arguments for the premises can be deleted safely, returning an “acceptable” argument for the conclusion. An argument is a pair ⟨∆, 𝔍⟩. Its validity on an atomic base 𝔅 is defined as follows:

∆ is closed ⇒
 it is a derivation in the atomic system of 𝔅 or
 it is in canonical form and, for every immediate subargument ∆^{*} of ∆, ⟨∆^{*}, 𝔍⟩ is valid over 𝔅 or
 by applying in some order the justifying procedures of 𝔍 to appropriate subargument skeletons of ∆, we hit upon a skeleton ∆^{*} in canonical form such that ⟨∆^{*}, 𝔍⟩ is valid over 𝔅; 
∆ is open ⇒ when we replace in ∆ unbound variables with closed terms from the language of 𝔅 and, for every expansion 𝔍^{+} of 𝔍, the closed unbound assumptions thereby obtained with any closed skeletons ∆^{*} for them such that ⟨∆^{*},𝔍^{+}⟩ is valid over 𝔅, we get an argument ⟨∆^{**},𝔍^{+}⟩ valid over 𝔅.
13In SVA, an inference is said to be valid when it yields valid arguments whenever applied to valid arguments. Thus, inferential validity depends on the global features of the skeletons where inferences occur –and relative justification procedures. However, in spite of the global character of their validity, introductions clearly have a privileged status.
 12 ^{ }For these points see A. Piccolomini d’Aragona, “Proofs, grounds and empty functions: epistemic co (...)
14In ToG, Prawitz overturns the SVA order of explanation of the notions of valid inference and proof. Valid inferences are now prior, while proofs are understood as finite chains of valid inferences. This is motivated by some philosophical reasons and achieved by means of two major changes.12 First, validity of inferences is defined locally in terms of epistemic grounds, i.e. objects that reify states where one is in possession of evidence for judgments or assertions. An inference is valid when a total constructive function exists from grounds for the premises to grounds for the conclusion. Second, an inference is understood, not as a mere passage from some premises to a given conclusion but, more strongly, as the application of an operation producing (alleged) grounds for the conclusion from (alleged) grounds for the premises.
 13 ^{ }A. Troelstra and D. van Dalen, Constructivism in mathematics vol. 2, Amsterdam, NorthHolland Pub (...)
15Atomic bases 𝔅 are defined as in SVA, and grounds for closed atomic formulas are again closed derivation for these formulas in 𝔅. Grounds over 𝔅 for closed 𝐴 can be then specified by induction on the logical form of 𝐴. The clauses are like those of the BHK semantics,13 since they associate to each logical constant 𝑘 a primitive operation 𝑘𝐼. As for ∧, e.g., we have that ∧𝐼(𝑔_{1},𝑔_{2}) is a ground over 𝔅 for 𝐴_{1} ∧ 𝐴_{2} if, and only if, 𝑔_{𝑖} is a ground over 𝔅 for 𝐴_{𝑖}, for 𝐴_{𝑖} closed (𝑖 = 1, 2). As for →, we have that → 𝐼ξ^{𝐴}(𝑓(ξ^{𝐴})) is ground over 𝔅 for 𝐴 → 𝐵 if, and only if, 𝑓(ξ^{𝐴}) is a 𝔅operation of type 𝐴 ⊳ 𝐵, for 𝐴 and 𝐵 closed –the primitive operation for → binds the typedvariable ξ^{𝐴}. However, this means that we need the further notion of typed operation on grounds over a base. A 𝔅operation on grounds of type
𝐴_{1}, …, 𝐴_{𝑚} ⊳ 𝐵
16is a total constructive function
𝑓 (𝑥_{1}, …, 𝑥_{n}, ξ^{𝐴}^{1}, …, ξ^{𝐴}^{m})
17– where 𝑥_{1},…, 𝑥_{n} are the individual variables occurring overall free in 𝐴_{1}, …, 𝐴_{𝑚}, 𝐵 – such that, for every ntuple of individuals 𝑘_{1}, …, 𝑘_{n} over the reference domain of 𝔅, for any 𝑔_{𝑖} ground over 𝔅 for 𝐴_{𝑖} [𝑘_{1}, …, 𝑘_{n}/𝑥_{1},…, 𝑥_{n}] (𝑖 ≤ 𝑚),
𝑓 (𝑘_{1}, …, 𝑘_{n}, 𝑔_{1}, …, 𝑔_{𝑚})
18is a ground over 𝔅 for 𝐵[𝑘_{1}, …, 𝑘_{n}/𝑥_{1},…, 𝑥_{n}]. We can then move on to higherorder operations of type
(Γ_{1} ⊳ 𝐴_{1}, …, Γ_{𝑛} ⊳ 𝐴_{𝑛}) ⊳ (∆ ⊳ 𝐵)
19– with ∆ included into the union of the Γ_{i}s – defined on lower level operations on grounds, and yielding lower level operations on grounds. Certain operations bind individual or typedvariables. The definitions are recursive, via compositionality of the primitive operations.
20Prawitz suggests the development of formal languages whose terms denote grounds or operations on grounds. The languages will contain variables typed on formulas, individual constants for closed atomic derivations, primitive operational symbols for the primitive operations involved in the groundclauses, and nonprimitive operational symbols for nonprimitive operations on grounds.
3.2. Semantics presuppositions
 14 ^{ }D. Prawitz, Natural deduction. A prooftheoretical study, New York, Dover Publications, 2006.
 15 ^{ }G. Gentzen, “Untersuchungen über das logische schließen”, art. cit.
21Prawitz’s semantics stems from a generalisation of Prawitz’s own normalisation theory.14 Prawitz normalisation theorems state that derivations in some natural deduction systems15 can be reduced to normal forms without detours. This requires some reduction rules that eliminate maximal (occurrences of) formulas, e.g.
 16 ^{ }Ibid.
22Like Gentzen’s Hauptsatz for sequent calculi,16 Prawitz’s theorems go beyond Hilbert’s reductive prooftheory, and belong to what Prawitz will later call general prooftheory: they do not aim at proving consistency of given systems by reducing them to other systems, but at reflecting upon general and structural properties of proofs, and thus at analysing what a proof is and how deductive activity is carried out.
 17 ^{ }Ibid.
23Prawitz’s normalisation still belongs to a level where provability is understood in formalistic terms, i.e. as derivability in a system. But some derived results suggest that Prawitz’s theorems may be connected with a semantic attitude. In particular, in intuitionistic logic one can prove what Schroeder Heister called fundamental corollary: any closed derivation reduces to one ending with an introduction. This is suggestive for it seems to confirm Gentzen’s wellknown claim that introductions establish the meaning of the logical constants, while eliminations are unique functions of the corresponding introductions.17 It is important to remark that we are here speaking of a formal result confirming an essentially informal claim: one adopts an informal point of view by “looking at”, or by “starting from” a formal fact.
 18 ^{ }For this point see e.g. L. Tranchini, “Prooftheoretic semantics, paradoxes and the distinction b (...)
24Of course, for the fundamental corollary to have its semantic weight, we need to conceive of normalisation as a justification process, not simply as a detourelimination process. We must conceive of reduction rules as justification procedures in SVA or operations on grounds in ToG  →reduction justifies (or is a non primitive operation for) →elimination. There is a gap between considering normalisation as a process that permits us to remove some redundant inferencesteps, and considering it as a process that permits us to compute the “justificationcore” of a derivation –normal derivations are sometimes understood in a Fregean sense as what nonnormal derivations denote.18 Moreover, we must be confident that what is suggested by results like the fundamental corollary holds for arbitrary formal setups as well.
25How to fill this gap? We cannot expect to be able to prove a “super normalisation theorem”, that is, normalisation for every possible formal setup. Like in Prawitz’s SVA or ToG, we must instead speak of arbitrary inferences and consider chains of inferences, not as formal objects, but as proofs. Conceptually, derivations are not the same as proofs. The former are obtained by combining mechanically given rules and axioms, while the latter have a deductive force stemming from meaning. Of course, derivations can be looked at as proofs, but this requires that rules and axioms enjoy some semantic justification.
26However, the understanding of formal results as a confirmation of informal claims is in Prawitz’s semantics not limited to Gentzen’s idea that introductions fix the meaning of the logical constants. Other semantic presuppositions allow for such a reading of normalisation.
 19 ^{ }M. Dummett, The logical basis of metaphysics, Cambridge, Harvard University Press, 1991; id., “Wh (...)
27For example, Prawitz’s semantics matches Dummett’s investigation into theory of meaning, in particular into the requisites that a satisfactory theory of meaning must comply with.19 Of course, we are here referring to Dummett’s claim that meaning should connect to a practice where knowledge of meaning can manifest itself. The epistemic bond given by the connection between meaning and knowledge of meaning is a sort of “informal axiom” of verificationist theories of meaning.
 20 ^{ }D. Prawitz, The validity of inference and argument, forthcoming.
 21 ^{ }D. Prawitz, Natural deduction…, op. cit.
28Other background tenets concern deduction. Deduction must be justified, i.e. semantics should not only provide a definition of logical consequence, but also explain why deduction exerts its epistemic power. This is a kind of distinction between an “extensional” way of conceiving of the aims of logic –producing a class of valid rules and formulas– and an “intensional” way of doing the same –explaining in what sense rules and formulas are valid. Observe that the explanatory task cannot be explicitly pursued within a formal system –to put it with Wittgenstein, we may say explanation is “shown” but not “told” by a formal system. Deduction must also be transparent, i.e. if something is a proof, we must be able to recognise that it is. This assumption has strong implications in the concrete development of constructive semantics. In particular, it led Prawitz to modify his approach several times. Prawitz’s recent investigations, e.g., focus on the “epistemic import” of justifying procedures.20 These procedures cannot provide a “vacuous” justification, as happens with inferences whose premises can have no justification. What this “epistemic import” is to be, is once again suggested by standard reduction rules for Gentzen’s eliminations, for they fit with the socalled inversion principle, and thus respect a containment constraint between argumentstructures.21
29These presuppositions seem to us to show that Prawitz’s semantics could be understood as a good instance of Kreisel’s informal rigour, provided one accepts the idea that the latter consists of a dialectic interaction between the intuitive and the formal level. Clearly, any semantics is inspired by some intuitive ideas. But in Prawitz these ideas are strictly tied to the formal level and, as said, confirmed by it; semantics is accordingly drawn from relevant formal results, by means of a suitable generalisation of these results.
3.3. A class of sound systems
30The interaction between the formal and the intuitive level in Prawitz’s SVA and ToG does not concern the semantic presuppositions only, but also how this semantics concretely articulates, its general framework and the results one can prove (or try to prove) about it.
31Prawitz’s provability is inexhaustibly wider than, and absolutely not reducible to formal derivability. This depends once again on inner properties of the formal setups, and in particular on Gödel’s incompleteness theorems. When discussing BHKprovability, Prawitz says for example that, although the clauses establishing what counts as a BHKproof run parallel to Gentzen’s introduction,
 22 ^{ }D. Prawitz, “Meaning and proofs: on the conflict between classical and intuitionistic logic”, The (...)
the conditions for asserting a sentence cannot be exhausted by any formal system […] there is no formal system generating all the procedures that transform canonical proofs of A to canonical proofs of B.22
32Of course, the reference is here to implications, whose BHKproofs are procedures that transform BHKproofs of the antecedent into BHKproofs of the consequent. By Gödel’s incompleteness results, there is no system capable of generating all such procedures on a base at least as rich as firstorder arithmetic. Thus, there is no system whose set of derivations corresponds to the class of BHKproofs.
 23 ^{ }D. Prawitz, “On the relation between Heyting’s and Gentzen’s approaches to meaning”, in T. Piecha (...)
 24 ^{ }W. Howard, “The formulaastypes notion of construction”, in J. R. Hindley, J. P. Seldin and P. J (...)
33It is easy to realise that Prawitz’s valid arguments and, above all, grounds may be understood as a sort of refinement of BHKsemantics –although some results by Prawitz show that these approaches may not be strictly “isomorphic”.23 Hence, what we said about BHKproofs holds for Prawitz’s valid arguments and grounds too. This is most evident in ToG where, as said, Prawitz envisages formal languages of grounds. Via the CurryHoward correspondence,24 any such language translates a system in a Gentzen’s natural deduction style where, additionally, each nonintroductory inference is justified by an appropriate SVA constructive procedure. Consequently,
 25 ^{ }D. Prawitz, “Explaining deductive inference”, art. cit., p. 98.
we know because of Gödel’s incompleteness result that already for first order arithmetical assertions there is no closed [i.e. recursive] language of grounds in which all grounds for them can be defined; for any such intuitively acceptable closed language of grounds, we can find an assertion and a ground for it that we find intuitively acceptable but that cannot be expressed within that language.25
 26 ^{ }D. Prawitz, “Towards a foundation of a general prooftheory”, art. cit.
34It is for this reason that Prawitz understands his languages as “open”, i.e. as indefinitely expandable through new symbols for new operations. The same may hold in SVA. The fact that languages of grounds are CurryHoward isomorphic to natural deduction systems where each nonintroductory inference comes with an SVA justification seems to suggest that these languages may be also understood as “linear” translations of what, in the SVA setup, Prawitz called justified deductive systems.26
 27 ^{ }Therefore, when we say that Prawitz’s provability is inexhaustibly wider than, and not reducible (...)
35So, no justified deductive system or language of grounds is complete with respect to valid arguments and grounds. However, when justified deductive systems and languages of grounds are sound, their derivations and terms constitute wellbehaving instances of the notions of valid argument and ground.27 The importance of this is not limited to correctness proofs. Sound formal setups also provide examples for further exploring and refining the intuitive notions. As said in Section 3.2, e.g., reduction rules for normalisation may suggest suitably strict –i.e. epistemically relevant– justifying procedures. Outside logic, mathematical induction shows that justifying procedures may not only rely upon logical properties, but also on the structure of the atomic base.
36In turn, this “informal refinement” suggests the possibility of extending sound formal setups in a hierarchic way. Although for each such setup there is a valid argument or ground not expressible within it, soundness implies that the setup can be extended by adding resources that comply with relevant intuitive properties. These properties are not in themselves fully expressible in the setups. Nonetheless, they permit us to find more and more accurate formalistic instances of valid arguments and grounds, in a neverending process of “approximation” of the set of formal derivations to the class of valid arguments and grounds. Examples of such properties are the already mentioned idea that valid nonintroductory inferences should respect some version of the inversion principle or, more generally, Dummett’s fundamental assumption, i.e. if something is a proof, then it must be reducible to a proof ending with an introduction –observe that this is the semantic version of the fundamental corollary of Section 3.2. Outside logic, we may think of reflection principles for justified deductive systems or languages of grounds over firstorder arithmetic.
37Also in this case, thus, we seem to have a strong dialectic interaction between the formal and the intuitive level. Intuitive notions overstep the formal counterparts, but the latter are instances that suggest a sharpening of the former, thereby permitting an improvement of our formal machinery.
4. Argument scheme and nonmonotonic reasoning
38In this section we concentrate on two different but related approaches to nonmonotonic reasoning. First, we introduce the notion of argument scheme, a keyconcept in Walton’s Argumentation Theory. Then, we briefly outline a formal justificationbased approach developed in AI for dealing with nonmonotonic reasoning. We conclude by arguing that, when compared, these approaches provide a seemingly necessary interplay between the formal and the informal level in the understanding of defeasibility.
4.1. Walton on argument scheme and presumptive reasoning
39In everyday conversation, people argue to support a claim by giving reasons for it and by defending these reasons against criticism. Walton’s Argumentation Theory aims at providing a model of rationality representing such interpersonal exchanges. A dialogue or conversation is conceived as
 28 ^{ }D. Walton, The New Dialectic: Conversational Contexts of Argument, Toronto, University of Toronto (...)
A goaldirected conventional framework where speech partners reason together in an orderly way, according to the rules of politeness or normal expectations of cooperative argumentation for the type of exchange they are engaged in.28
 29 ^{ }Ibid.
40One common form of move in a dialogue is an argument, where one or more premises are put forward to support a conclusion or to bear on an unsettled issue. In Walton’s theoretic framework,29 arguments are evaluated as correct or incorrect according to whether they contribute to, or else impede, the goals of the dialogue.
41In ordinary linguistic exchange, we confront with different kinds of arguments and different ways in which a conclusion can be supported by premises. This may happen through a deductively valid argument where, if the respondent accepts the premises, she must accept the conclusion. In many others cases, such a perfection is not attainable: our grounds may provide less than conclusive evidence for the conclusion, that is, they may provide evidence for tentatively accepting the conclusion of the argument given the information known in the conversational context, without ruling out the possibility of subsequently retracting it as new information comes in. In employing such arguments –fallible and inherently subject to default– our reasoning might fall into those kinds of argumentation that have been historically classified as fallacious.
 30 ^{ }D. Walton. A Pragmatic Theory of Fallacy, Tuscaloosa, University of Alabama Press, 1995.
 31 ^{ }D. Walton, Argumentation Schemes for Presumptive Reasoning, Mahwah, NJ, Lawrence Elbraum Associat (...)
42One of the main tenets of Walton’s theory concerns the status of fallacies within conversational context. Walton maintains30 that major traditional fallacies should be considered as species of argumentation that are not inherently incorrect in every instance of their use. Although such arguments can sometimes be fallacious, on other occasions they appear as reasonable: an appeal to expert opinion could be reasonable and provide grounds for accepting the conclusion, although the same general form of argument may sometimes constitute a fallacious appeal to authority. The support is thus tentative and inconclusive while still being strong enough, in many cases, to have some degree of bindingness.31
43Because of the impossibility of analysing them through deductive logic, a systematic study of these forms of argument requires some theoretical tools. Argumentation schemes represent a quasiformal device to fulfil the goal. They are stereotypical patterns of reasoning used in everyday exchanges, consisting of a set of premises and a conclusion that is presumed to follow from them. As an example, we can consider the scheme for the argument from position to know:
Pr_{1}: a is in a position to know that A
Pr_{2}: a asserts that A is true
Conc: A is true
 32 ^{ }Ibid., Chap. 3; D. Walton, C. Reed and F. Macagno, Argumentation Schemes, Cambridge, Cambridge Un (...)
 33 ^{ }B. Verheij, “Logic, context and valid inference. Or: Can there be a logic of law?”, in H. Jaap va (...)
44As many of the defeasible argument schemes identified by Walton,32 the scheme is modelled on defeasible modus ponens. Walton introduces such a definition following the distinction advanced by Verheij33 between the familiar modus ponens of deductive inference and modus non excipiens. According to this distinction, in the former, the first premise does non admit exceptions since it is based on a strict –nondefeasible rule– while, in the latter, the first premise could be based on a rule which admits that an exception might come into play defeating it. The defeasible modus ponens turns out to be the basis for other defeasible inferences concerning knowledgebased arguments, so that any argumentation in concrete verbal exchange fitting with it can be analysed according to this general and abstract form.
 34 ^{ }D. Walton and F. Macagno, “A classification system for argumentation schemes”, Argument and Compu (...)
45Argument schemes represent a necessary tool for many of the desiderata of Argumentation Theory, i.e. identifying and classifying arguments, analysing them and finding missing premises.34 Walton aims at providing a normative analysis, where the crucial question is whether and how these schemes can function to test correctness of their instances in natural language argumentation.
 35 ^{ }D. Walton, Argumentation Schemes for Presumptive Reasoning, op. cit.
46A common feature shared by argumentation schemes is that they represent a distinct type of reasoning, which Walton calls presumptive reasoning. This includes arguments that are plausible in nature, meaning that if the premises are true or acceptable, then the conclusion does not follow deductively, but only as a reasonable presumption in given circumstances, and is subject to retraction if these circumstances change.35 For, instances of defeasible schemes are not compelling as deductive arguments are. The respondent may always raise critical questions before accepting their conclusion; if an argument meets the requirements of a scheme, and if the respondent accepts the premises, she is forced to accept the conclusion. But such acceptance is only provisional. If the respondent makes a critical and appropriate question, and the proponent fails to offer an adequate answer, the argument defaults and the proponent must retract it. Thus, the basic way a presumptive argument operates in a dialogue is through some provisional basis for going ahead, even in the absence of firm premises known to be true. So, the presumptive nature of these arguments essentially implies that the proponent does not have a burden of proof, but only a burden of disprove contrary evidence which might arise in the future sequence of a dialogue.
47The evaluation of argumentation schemes thus depends on the conversational context where they are used, as well as on two keyconcepts of Walton’s theory: critical questions  questions by which an argument based on a scheme might be judged to be good or fallacious –and burden of proof– the obligation of each party to prove, disprove or question some particular propositions.
 36 ^{ }Ibid., p. 62; D. Walton, C. Reed and F. Macagno, Argumentation Schemes, op. cit., p. 309.
48In order to provide a normative account of how argumentation works within dialogues, any argumentation scheme must be supplemented by a set of specific critical questions. In the case of argument from position to know they are the following:36
Q_{1}: Is a in a position to know whether A is true?
Q_{2}: Is a a honest source?
Q_{3}: Did a assert that A is true?
49While the first and the third question directly challenge the premises of the argument, the second question points to –and at the same time reveals– an assumption of the argument, that is, that the source of knowledge is trustworthy.
50Thus, the role of argument schemes in evaluating arguments is essentially dialogical: an argument is a move in a dialogue and the scheme that it instantiates determines the allowed and required response to that move by the other side. For an argument to be justified it is not sufficient it fits with a recognised argument scheme: it should also survive a dialogical process of critical examination.
 37 ^{ }C. Reed and D. Walton, “Argumentation Schemes in Dialogue”, in H.V. Hansen et al. (eds.), Dissens (...)
 38 ^{ }D. Walton, C. Reed and F. Macagno, Argumentation Schemes, op. cit., p. 364 sqq.
 39 ^{ }K. Atkinson, T. BenchCapon, F. Bex, T.F. Gordon, H. Prakken, G. Sartor and B. Verheij, “In memor (...)
51This philosophical enterprise seems to possess an essentially informal and pragmatic nature, far from the formal machinery of deductive logic. However, Walton devotes many reflections to how formalisation might contribute to a better understanding of this forms of reasoning.37 He explicitly speaks of strong formalisation 38 when he refers to the possibility of formalising each scheme as an inferencestructure similar to those we are already familiar with in deductive logic. Many possibilities to accomplish the goal, born from the interaction of different research fields such as artificial intelligence, computer technologies and legal reasoning, have been and are still explored.39
 40 ^{ }L. Amgoud, M. Caminada, C. Cayrol, M.C. Lagasquie and H. Prakken, “Towards a consensual formal mo (...)
 41 ^{ }C. Reed and G. Rowe, “Araucaria: Software for Argument Analysis, Diagramming and Representation”, (...)
 42 ^{ }D. Walton and T.F. Gordon, “Formalizing Informal Logic”, Informal Logic, vol. 35, n^{o} 4, 2015, p. (...)
52In the next section, we will concentrate on a formal system belonging to those approaches that aim at representing argument schemes and their properties through a standard model for defeasible argumentation. Specifically, our attention will be devoted to ASPIC+, a formal framework originated from the European Aspic Project and originally intended to integrate the main approaches to structured argumentation.40 The rationale of our choice lies upon the fact that such a system supplies a formalisation of arguments that resembles the way a deductive logical system operates, suggesting a starting point for further developments of new argumentation logics. Even though they will not be part of our discussion, it is worth mentioning two other distinct approaches to the project of formalising Walton’s notion of argument scheme: Araucaria and Carneades. Araucaria41 is a software tool which provides a diagramming process, supported by the Argument Markup Language designed in XML, as well as an analysis of arguments via identification of their structure in terms of their components and of the relationship among them. The formalisation involved in such a system, albeit purely descriptive, is necessary to supply a formal characterization of the analytical component the software needs to store and manipulate. Carneades42 is a formal computational model developed for dealing with legal reasoning. The model is built on ontologies from the semantic web and represents arguments as directed labelled graphs. Although this computational tool cannot be mechanically applied to arguments to produce automatic evaluation, it can help users to carry out the task of critically assessing them by representing their features within a formal structure. The distinct perspectives provided by ASPIC+, Araucaria and Carneades offer alternative insights into how a formal treatment of the informal features of arguments in conversational context can be philosophically relevant for a better understanding of them; at the same time, they pose a further challenge, which will not be addressed here, i.e., the possibility of reflecting upon how such systems might interact with each other.
4.2. A formalisation of nonmonotonic reasoning
 43 ^{ }P.M. Dung, “On the acceptability of arguments and its fundamental role in non monotonic reasoning (...)
 44 ^{ }H. Prakken, “An overview of formal models of argumentation and their application in philosophy”, (...)
53ASPIC+ is a formal argumentation framework developed in AI for the study of nonmonotonic reasoning. It is based on the abstract argumentation framework presented by Dung43 which consists in a pair ⟨𝐴, Def⟩ where 𝐴 is a set of arguments and Def is a binary relation of defeat on 𝐴. In Dung’s framework, a sequence of arguments is modelled in a directed graphstructure where arguments are related to others by the defeat relation. However, the notion of argument employed is entirely abstract and has no features other than the defeat relation.44 ASPIC+ is thus just an instantiation of Dung’s framework, providing guidance on the structure of arguments, the nature of attacks and the use of preferences. The framework is based on a logical language 𝐿 equipped with a set of strict and defeasible rules, which generates argumentationsequences in the form of treestructures. An inference rule is strict when, if its antecedents are accepted, the consequent must be accepted no matter what, while an inference rule is defeasible when, if its antecedents are accepted, its consequent must be accepted, if there are no good contrary reasons.
 45 ^{ }J. Pollock, “Defeasible Reasoning”, Cognitive Science, n^{o} 11, 1987, p. 481518.
54Central for the construction of the system is Pollock’s epistemological distinction between two kinds of defeater: the rebutting defeater, who attacks the conclusion of a defeasible inference, and the undercutting defeater, who attacks the defeasible inference as such.45 The basic idea is that
 46 ^{ }H. Prakken and G. Sartor, “Argumentbased extended logic programming with defeasible priorities”, (...)
Nonmonotonic reasoning can be analysed in terms of the interactions between arguments for alternative conclusions […] nonmonotonicity, or defeasibility, arises from the fact that arguments can be defeated by stronger counterarguments.46
55Despite the general and abstract nature of the framework, which applies to any set of strict and defeasible rules and allows to adopt different semantics for defining the acceptability status of arguments, to account for conflicts between arguments, we should assume that 𝐿 should contain a binary contrariness relation on wff of 𝐿, indicated with –.
 47 ^{ }S. Modgil and H. Prakken, “The ASPIC+ framework for structured argumentation: a tutorial”, Argume (...)
56In the presentation of the formal structure of APSIC+ we mainly follow the one proposed by Modgil and Prakken.47 The basic notion is that of argumentation system:

An argumentation system is a triple AS = ⟨𝐿, R, n⟩ where

𝐿 is a language closed under negation (¬);

R = R_{s} ∪ R_{d} is a set of strict (R_{s}) and defeasible (R_{d}) inference rules of the form 𝜑_{1},…, 𝜑_{n}→ 𝜑 and 𝜑_{1},…, 𝜑_{n}⇒ 𝜑 respectively (where 𝜑_{i}, 𝜑 are metavariables ranging over wff in 𝐿), and such that R_{s} ∩ R_{d} = ∅;

n is a partial function such that n: R_{d} → 𝐿.
57Informally, n(r) is the function that names defeasible rules in 𝐿, saying that the defeasible rule r ∈ R is applicable. We write 𝜑 = – 𝜓 just in case 𝜓 = ¬𝜑 or 𝜑 = ¬𝜓. Next we have knowledge bases 𝐾, that specifies the premises from which arguments can be built. 𝐾 is the union set of two disjoint kind of wff: axioms 𝐾_{n} (which are certain and cannot be attacked) and ordinary premises 𝐾_{p} (which are uncertain and, so, can be attacked). We can then combine an argumentation system and a knowledge base to obtain an Argumentation Theory:

An Argumentation Theory is a pair AT = ⟨AS, 𝐾⟩ where AS is an argumentation system and 𝐾 is a knowledge base in AS.
58Given AT, arguments can be now defined as chained applications of inference rules in AS, starting with elements from 𝐾. Any argument can be associated to the following functions: Prem, which returns as value all the formulas of 𝐾 used to build the argument –i.e. the premises; Conc, which returns its conclusion; Sub, which returns all its subarguments; DefRules, which returns all the defeasible rules of the argument; and TopRules which returns the last inference rule used in the argument. More specifically:

An argument 𝐴 on the basis of an AT with a knowledge base 𝐾 and an argumentation system ⟨𝐿, R, n⟩ is:

𝜑 if 𝜑 ∈ 𝐾 with: Prem(𝐴) = {𝜑}, Conc(𝐴) = {𝜑}, Sub(𝐴) = {𝜑}, DefRules (𝐴) = ∅, TopRules(𝐴) = undefined.

𝐴_{1},…,𝐴_{n} → 𝜓 if 𝐴_{1},…,𝐴_{n} are arguments such that there is a strict rule Conc(𝐴_{1}),…,Conc(𝐴_{n}) → 𝜓 in 𝑅_{s} with:
Prem(𝐴) = Prem(𝐴_{1}) ∪…∪ Prem(𝐴_{n}),
Conc(𝐴) = 𝜓,
Sub(𝐴) = Sub(𝐴_{1}) ∪…∪ Sub(𝐴_{n}) ∪ {𝐴},
DefRules(𝐴) = DefRules(𝐴_{1}) ∪…∪ DefRules(𝐴_{n}),
TopRule(𝐴) = Conc(𝐴_{1}),…,Conc(𝐴_{n}) → 𝜓. 
𝐴_{1},…,𝐴_{n} ⇒ 𝜓 if 𝐴_{1},…,𝐴_{n} are arguments such that there is a defeasible rule Conc(𝐴_{1}),…,Conc(𝐴_{n}) ⇒ 𝜓 in 𝑅_{d} with:
Prem(𝐴) = Prem(𝐴_{1}) ∪…∪ Prem(𝐴_{n}),
Conc(𝐴) = 𝜓,
Sub(𝐴) = Sub(𝐴_{1}) ∪…∪ Sub(𝐴_{n}) ∪ {𝐴},
DefRules(𝐴) = DefRules(𝐴_{1}) ∪…∪ DefRules(𝐴_{n}) ∪{Conc(𝐴_{1}),…,Conc(𝐴_{n}) ⇒ 𝜓},
TopRule(𝐴) = Conc(𝐴_{1}),…,Conc(𝐴_{n}) ⇒ 𝜓.
59Four types of arguments can be now identified: strict if DefRules(𝐴) = ∅; defeasible if DefRules(𝐴) ≠ ∅; firm if Prem(𝐴) ⊆ 𝐾_{n}; and plausible if Prem(𝐴) ∩ 𝐾_{p} ≠ ∅.
60We can now define the attack relation, the formal counterpart of the notion of conflict between arguments. ASPIC+ allows us to model three distinct types of attack; the already mentioned rebutting and undercutting, and a third type of attack against ordinary premises of a general inference step –which we call undermining attack. The rationale behind the introduction of undermining attack lies in the need to cover possible attacks raised against a deductive inference. Since the truth of the premises of a strict inference implies necessarily the truth of the conclusion, arguments cannot be attacked on the conclusion of a strict inference. Therefore, any doubt about the truth of the conclusion of a deductive inference implies there must be something wrong with its premises. Formally:

𝐴 attacks 𝐵 iff 𝐴 undercuts, rebuts, undermines 𝐵, where:
 𝐴 undercuts 𝐵 (on 𝐵’) iff Conc(𝐴) = – 𝑛(𝑟) for some 𝐵’∈ Sub(𝐵) such that 𝐵’ top rule 𝑟 is defeasible;
 𝐴 rebuts 𝐵 (on 𝐵’) iff Conc(𝐴) = – 𝜑 for some 𝐵’∈ Sub(𝐵) such that 𝐵’’_{1},…, 𝐵’’_{n} ⇒ 𝜑; and
 𝐴 undermines 𝐵 (on 𝜑) iff Conc(𝐴) = – 𝜑 for an ordinary premises 𝜑 of 𝐵.
 48 ^{ }S. Modgil and H. Prakken, “The ASPIC+ framework…”, art. cit., p. 40.
61Just few remarks about the attack relation. First, attacks can only be directed to fallible elements of the attacked arguments. Second, the definition poses a distinction between preferencedependent and preferenceindependent attack: only the success of rebutting and undermining attacks is contingent on preferences; since an argument using 𝑟 is undercut by any argument with conclusion – 𝑛(𝑟), undercutting attack succeeds as a defeat independently of any preference set.48
 49 ^{ }H. Prakken and G. Sartor, “Argumentbase extended logic programming…”, art. cit.
62Two conflicting arguments cannot be both justified, so we can understand the attack relation as a relation between arguments and counterarguments.49 We can thus say that an argument 𝐴 is a counterargument of 𝐵, if 𝐴 successful attacks 𝐵, i.e. defeats 𝐵. Whether an attack from 𝐴 to 𝐵 (on its subarguments 𝐵’) actually defeats 𝐵 may depend on the relative strength of 𝐴 and 𝐵’, i.e. on whether 𝐵’ is strictly stronger or strictly preferred to 𝐴. So, the definition of a defeat relation requires a preference ordering over arguments, indicated with ⪯: if 𝐴 ⪯ 𝐵 and 𝐵 ⪯ 𝐴, then 𝐵 is strictly preferred to 𝐴 (denoted by 𝐵 ≺ 𝐴) and, if 𝐴 ⪯ 𝐵 and 𝐵 ⪯ 𝐴, then 𝐴 ≈ 𝐵. Thus, successful attacks –the defeat relation– can be defined as follows:

𝐴 successfully rebuts 𝐵 if 𝐴 rebuts 𝐵 on 𝐵’and 𝐴 ⊀ 𝐵’;

𝐴 successfully undermines 𝐵 if 𝐴 undermines 𝐵 on 𝜑 and 𝐴 ⊀ 𝜑; and

𝐴 defeats 𝐵 if 𝐴 undercuts or successfully rebuts or successfully undermines 𝐵.
4.3. Defeasibility between formal and informal level
 50 ^{ }H. Prakken, “On the nature of argument scheme”, in C. Reed and C. Tindale (eds.), Dialectics, dia (...)
63We are now in the position to evaluate the contribution the structured argumentation framework may supply to the formalisation of argument schemes. As Prakken suggests,50 a natural way to formalise reasoning with argument schemes is to regard them as defeasible inference rules and to regard critical questions as pointers to counterargument.
64If we refer to the scheme for argument from position to know presented in the previous section, we may consider questions 1 and 2 as pointing to undermine premises 1 and 2 respectively, while question 3 as pointing to undermine the argument. Accordingly, we formalise the scheme and its undercutter as follows:
𝑑_{w}(𝑥, 𝜑) : PositionToKnow (𝑥, 𝜑), Says (𝑥, 𝜑) ⇒ 𝜑
𝑢_{w}(𝑥, 𝜑) : ¬ Credible (𝑥) ⇒ ¬ 𝑑_{w}(𝑥, 𝜑)
65where 𝑥 is replaced by a ground term denoting a specific agent and 𝜑 by a specific state of affairs.
66The interplay between the informal and the formal level in the analysis of argument schemes can be seen as an instance of informal rigour. Although they are not concerned with the intuitive counterpart of a mathematical notion, Walton’s argumentation schemes and the formal setup developed in AI are both meant to investigate how reasonable arguments that cannot be analysed as deductively valid, could provide support to their conclusion. Both approaches can be conceived as different attempts to solve the same problem: defeasibility of arguments in ordinary contexts. Starting from intuitions about the very nature of arguments outside the pristine realm of mathematics, the notion of argument schemes and the structured framework ASPIC+ aim at providing, “with the means available”, as Kreisel says, a theoretical analysis of this intuitive notion.
 51 ^{ }For a possible development of this interpretation, see, for instance, H. Prakken, “On the nature (...)
67The dialectical exchange –which we have indicated as a decisive feature of the informal rigour– forces both analyses to move step forwards. The notion of argument scheme understood in terms of defeasible inference rule is clearly a monological one, while Walton’s notion is essentially dialogical and strictly connected to a dialectical process of testing. The former assumes a single and fixed information, while the latter sees contexts as equipped with distributed and possibly changing information. To reconcile these two views, a possible route is to embed the formal framework in a dialogical setting identifying counterarguments through a dialogical process and considering dialogues as providing the relevant statements and arguments at each stage, and logic as determining the justified arguments at that stage.51
 52 ^{ }M. Caminada and L. Amgoud, “On the evaluation of argumentation formalisms”, Artificial Intelligen (...)
 53 ^{ }Indirect consistency is defined in terms of the closure of a set of wellformed formulas under ap (...)
 54 ^{ }S. Modgil and H. Prakken, “A general account of argumentation with preferences”, art. cit.
68Moreover, the move towards strong formalisation in Walton’s sense, allows us to study properties that one would intuitively expect to hold of arguments from an extensional point of view. We can prove that logical systems built on ASPIC+ satisfy the rationality postulates proposed by Caminada and Amgoud52 –general constraints that any ruledbased argumentation formalism should satisfy. They guarantee, for example, that the conclusions of all arguments in the same extension are mutually consistent and closed under the application of strict inference rules. This is achieved by requiring that direct consistency and indirect consistency53 can be defined in the system, and that the preference ordering is reasonable, namely:54

arguments that are both strict and firm are strictly preferred over all other arguments;

the strength of an argument is determined exclusively by the defeasible rules and/or ordinary premises;

the preference order is acyclic, i.e. if 𝐵 ≺ 𝐴, then it must be that 𝐵’ ≺ 𝐴 where 𝐵’ is some maximal defeasible subarguments of 𝐵.
 55 ^{ }D. Walton and T.F. Gordon, “Formalizing Informal Logic”, art. cit.
69The main motivation for passing from the informal level to the formal one comes from the normative side of Walton’s analysis and is closer to our interpretation of Kreisel’s informal rigour: the possibility of formalising argument schemes permits the introduction of standard of proof for arguments in conversational context, that is, the establishment of degrees of strength for an argument to be a proof.55
5. Conclusion
70To conclude we just make two observations. First, Prawitz’s semantics belongs to the broader and lively field of prooftheoretic semantics. One may then wonder whether the idea put forward in this paper –Prawitz’s semantics as a good instance of Kreisel’s informal rigour– may be extended also to other proofbased semantic approaches. Second, in the field of Argumentation Theory –strictly linked to the philosophy of mathematical practice– the mistrust towards formal methods is widespread. However, as our interpretation suggests, Walton’s analysis contains ingredients of informal rigour that points to the theoretical role of the formal moment even for such informal philosophical enterprise and, at the same time, to further developments of the logical setting for nonmonotonic reasoning to deal with arguments in ordinary contexts.
 56 ^{ }In a nutshell, the dialectical interaction between the formal and the informal level may be expla (...)
71Overall, the interpretation we have proposed allows for an approach to objectivity in mathematics which is in a way alternative –or, less strongly, complementary– to the one upheld by most of the “philosophy of mathematical practice”. As shown by the connection between Kreisel’s informal rigour, on the one hand, and Prawitz’s semantics and Walton’s Argumentation Theory, on the other, one had better not overreact against the formal moment. Formalisation and its (meta)properties may not be mere “nominalistic” stances, but convey a strong conceptual content. And this, not simply in the sense of being inspired by some informal desiderata but, more significantly, in that of confirming certain semantic claims. Thus, an entire semantics might be understood as nothing but a generalisation of (relevant structural features) of given formal systems. Conversely, the limits of formalisation, when overcome semantically, may suggest an improvement of the formal moment. It is precisely thanks to these limits that sound systems hint at principles which may serve for refining the formal analysis itself. The validity of these principles can be seen and dealt with semantically, in a broader context where families of more and more powerful formal setups approximate to completeness relatively to a given domain.56
 57 ^{ }G. Crocco, “Informal and absolute proofs…”, art. cit.
72It seems to us that Prawitz’s semantics and Walton’s Argumentation Theory, when understood as good instances of Kreisel’s informal rigour, provide support for the standpoint we have just described. Of course, this presupposes one accepts our reconstruction of Kreisel’s informal rigour (and the one inspiring it).57 Besides that, one may also ask whether our kreiselian reading of Prawitz and Walton allows for some advancements within their semantics and Argumentation Theory, respectively. We remark that everything we said about these two theories is already contained in Prawitz’s and Walton’s writing. However, the perspective on these theories is seemingly new. Thus, we leave it open whether this perspective may trigger some developments in prooftheoretic semantics or Argumentation Theory.
Notes
1 ^{ }G. Crocco, “Informal and absolute proofs: some remarks from a Gödelian perspective”, in G. Crocco and A. Piccolomini d’Aragona (eds.), Inferences and proofs, special issue of Topoi, 2019, p. 561575.
2 ^{ }G. Kreisel, “Informal rigour and completeness proofs”, in I. Lakatos (ed.), Problems in the philosophy of mathematics, Amsterdam, NorthHolland Publishing Company, 1967, p. 138186.
3 ^{ }G. Kreisel, “Ordinal logics and the characterization of informal concepts of proof”, in J. A. Todd (ed.), Proceedings of the international congress of mathematicians 1421 Aug. 1958, Edinburgh, Cambridge University Press, 1958, p. 289299; G. Kreisel, “Church’s thesis and the idea of informal rigour”, Notre Dame Journal of Formal Logic, vol. 28, n^{o} 4, 1987, p. 499519.
4 ^{ }G. Kreisel, “Informal rigour and completeness proofs”, art. cit., p. 138.
5 ^{ }Id., p. 138.
6 ^{ }Id., p. 138.
7 ^{ }N. Barton, “Structural relativity and informal rigour”, in G. Oliveri, S. Boscolo and C. Ternullo (eds.), Objects, structures and logics, BerlinHeidelbergNew York, Boston studies in the philosophy and history of science, Springer, 2022.
8 ^{ }For this see e.g. M. Antonutti Marfori, “Informal proofs and mathematical rigor”, Studia Logica, vol. 96, n^{o} 2, 2010, p. 261272.
9 ^{ }A defence of this interpretation can be found in G. Crocco, “Informal and absolute proofs…”, art. cit.
10 ^{ }For the semantics of valid arguments we mainly refer to D. Prawitz, “Towards a foundation of general prooftheory”, in P. Suppes (ed.), Logic methodology and philosophy of science IV, Amsterdam, NorthHolland Publishing Company, 1973, p. 225250. For the theory of grounds, we mainly refer to D. Prawitz, “Explaining deductive inference”, in H. Wansing (ed.), Dag Prawitz on proofs and meaning, BerlinHeidelbergNew York, Springer, 2015, p. 65100.
11 ^{ }G. Gentzen, “Untersuchungen über das logische schließen”, Matematische Zeitschrift, vol. 39, 19341935.
12 ^{ }For these points see A. Piccolomini d’Aragona, “Proofs, grounds and empty functions: epistemic compulsion in Prawitz’s semantics”, Journal of philosophical logic, 2021.
13 ^{ }A. Troelstra and D. van Dalen, Constructivism in mathematics vol. 2, Amsterdam, NorthHolland Publishing, 1988.
14 ^{ }D. Prawitz, Natural deduction. A prooftheoretical study, New York, Dover Publications, 2006.
15 ^{ }G. Gentzen, “Untersuchungen über das logische schließen”, art. cit.
16 ^{ }Ibid.
17 ^{ }Ibid.
18 ^{ }For this point see e.g. L. Tranchini, “Prooftheoretic semantics, paradoxes and the distinction between sense and denotation”, Journal of Logic and Computation, vol. 26, n^{o} 2, 2016, p. 495512.
19 ^{ }M. Dummett, The logical basis of metaphysics, Cambridge, Harvard University Press, 1991; id., “What is a theory of meaning? (I)”, in M. Dummett, The seas of language, Oxford, Oxford University Press, 1996, p. 133.
20 ^{ }D. Prawitz, The validity of inference and argument, forthcoming.
21 ^{ }D. Prawitz, Natural deduction…, op. cit.
22 ^{ }D. Prawitz, “Meaning and proofs: on the conflict between classical and intuitionistic logic”, Theoria, vol. 43, n^{o} 1, 1977, p. 240, p. 29.
23 ^{ }D. Prawitz, “On the relation between Heyting’s and Gentzen’s approaches to meaning”, in T. Piecha and P. SchroederHeister (eds.), Advances in prooftheoretic semantics, BerlinHeidelbergNew York, Springer, 2016, p. 525.
24 ^{ }W. Howard, “The formulaastypes notion of construction”, in J. R. Hindley, J. P. Seldin and P. Jonathan (eds.), To H. B. Curry: essays on combinatory logic, lambda calculus and formalism, London, Academic Press, 1980, p. 479490.
25 ^{ }D. Prawitz, “Explaining deductive inference”, art. cit., p. 98.
26 ^{ }D. Prawitz, “Towards a foundation of a general prooftheory”, art. cit.
27 ^{ }Therefore, when we say that Prawitz’s provability is inexhaustibly wider than, and not reducible to formal derivability, we mean what follows. Let 𝔅 be a base at least as powerful as a base for firstorder arithmetic, and let us indicate with Γ =_{𝔅} 𝐴 that there is an argument from Γ to 𝐴 which is valid over 𝔅, or a ground over 𝔅 of type Γ ⊳ 𝐴. Then, Gödel’s incompleteness theorems imply that there is no recursive (consistent) system Σ over 𝔅 such that Π_{𝔅} = T_{Σ}, where Π_{𝔅} = {(Γ,𝐴)  Γ=_{𝔅} 𝐴} and T_{Σ} = {(Γ, 𝐴)  Γ ⊢_{Σ} A} –this also implies that there is no recursive (consistent) system Σ over 𝔅 such that Ω_{𝔅} = DER_{Σ}, where Ω_{𝔅} = {ε  ε is a valid argument or ground over 𝔅} and DER_{Σ} = {∆  ∆ is a derivation in Σ}. Of course, one may expect that, if (Γ, 𝐴) ∈ Π_{𝔅}, then there is a recursive (consistent) system Σ over 𝔅 such that (Γ, 𝐴) ∈ T_{Σ}, and similarly that if ε ∈ Ω_{𝔅}, then there is a recursive (consistent) system Σ over 𝔅 such that ε = ∆ for some ∆ ∈ DER_{Σ} (given an appropriate notion of identity for proofs). However, one cannot also expect the class of recursive (consistent) systems over 𝔅 to be recursively enumerable –otherwise, the class of firstorder arithmetic truths would be recursively enumerable too. So, the simple existence of some such Σ is not sufficient for claiming that we can reduce =_{𝔅} to ⊢_{Σ}, and the property of being a valid argument or ground over 𝔅 to that of being a derivation in Σ. We remark that this line of thought holds implicitly in Prawitz’s writings, although Prawitz never concludes from this that his notion of provability is inexhaustibly wider than, and absolutely not reducible to formal derivability. We leave it open whether Prawitz would understand what we said as meaning that his semantic notion of provability can by no means reduce to the formal notion of derivability.
28 ^{ }D. Walton, The New Dialectic: Conversational Contexts of Argument, Toronto, University of Toronto Press, 1998, p. 3.
29 ^{ }Ibid.
30 ^{ }D. Walton. A Pragmatic Theory of Fallacy, Tuscaloosa, University of Alabama Press, 1995.
31 ^{ }D. Walton, Argumentation Schemes for Presumptive Reasoning, Mahwah, NJ, Lawrence Elbraum Associates, 1996, p. 10.
32 ^{ }Ibid., Chap. 3; D. Walton, C. Reed and F. Macagno, Argumentation Schemes, Cambridge, Cambridge University Press, 2008, Chap. 9.
33 ^{ }B. Verheij, “Logic, context and valid inference. Or: Can there be a logic of law?”, in H. Jaap van der Herik et al. (eds.), Legal Knowledge Based Systems. JURIX 1999, The Twelfth Conference, Nijmegen, 1999, p. 109121.
34 ^{ }D. Walton and F. Macagno, “A classification system for argumentation schemes”, Argument and Computation, vol. 6, n^{o} 3, 2016, p. 219245.
35 ^{ }D. Walton, Argumentation Schemes for Presumptive Reasoning, op. cit.
36 ^{ }Ibid., p. 62; D. Walton, C. Reed and F. Macagno, Argumentation Schemes, op. cit., p. 309.
37 ^{ }C. Reed and D. Walton, “Argumentation Schemes in Dialogue”, in H.V. Hansen et al. (eds.), Dissensus and the Search for Common Ground, Windsor, 2007, p. 111.
38 ^{ }D. Walton, C. Reed and F. Macagno, Argumentation Schemes, op. cit., p. 364 sqq.
39 ^{ }K. Atkinson, T. BenchCapon, F. Bex, T.F. Gordon, H. Prakken, G. Sartor and B. Verheij, “In memoriam of Douglas N. Walton: the influence of Doug Walton on AI and law”, Artificial Intelligence, n^{o} 28, 2020, p. 281326.
40 ^{ }L. Amgoud, M. Caminada, C. Cayrol, M.C. Lagasquie and H. Prakken, “Towards a consensual formal model: inference part”, Deliverable D2.2 of Aspic Project, 2004.
41 ^{ }C. Reed and G. Rowe, “Araucaria: Software for Argument Analysis, Diagramming and Representation”, International Journal of Artificial Intelligence Tool, vol. 10 n^{o} 4, 2004, p. 961979.
42 ^{ }D. Walton and T.F. Gordon, “Formalizing Informal Logic”, Informal Logic, vol. 35, n^{o} 4, 2015, p. 508538.
43 ^{ }P.M. Dung, “On the acceptability of arguments and its fundamental role in non monotonic reasoning, logic programming and nperson games”, Artificial Intelligence, vol. 77, n^{o} 2, 1995, p. 321257.
44 ^{ }H. Prakken, “An overview of formal models of argumentation and their application in philosophy”, Studies in logic, vol. 4, n^{o} 1, 2011, p. 6586.
45 ^{ }J. Pollock, “Defeasible Reasoning”, Cognitive Science, n^{o} 11, 1987, p. 481518.
46 ^{ }H. Prakken and G. Sartor, “Argumentbased extended logic programming with defeasible priorities”, Journal of Applied NonClassical Logic, vol. 7, n^{o} 1/2, 1997, p. 2575, p. 28.
47 ^{ }S. Modgil and H. Prakken, “The ASPIC+ framework for structured argumentation: a tutorial”, Argument and Computation, vol. 5, n^{o} 1, 2014, p. 3162.
48 ^{ }S. Modgil and H. Prakken, “The ASPIC+ framework…”, art. cit., p. 40.
49 ^{ }H. Prakken and G. Sartor, “Argumentbase extended logic programming…”, art. cit.
50 ^{ }H. Prakken, “On the nature of argument scheme”, in C. Reed and C. Tindale (eds.), Dialectics, dialogue and argumentation. An examination of Douglas Walton’s theories of reasoning and argument, London, College Publishing, 2010; H. Prakken, “An overview of formal models…”, art. cit.; S. Modgil and H. Prakken, “The ASPIC+ framework…”, art. cit.
51 ^{ }For a possible development of this interpretation, see, for instance, H. Prakken, “On the nature of argument scheme”, art. cit.; id., “An overview of formal models…”, art. cit.
52 ^{ }M. Caminada and L. Amgoud, “On the evaluation of argumentation formalisms”, Artificial Intelligence, vol. 171, n^{o} 5/6, 2007, p. 286310.
53 ^{ }Indirect consistency is defined in terms of the closure of a set of wellformed formulas under application of strict inference rules, that is, the strict closure of a set of wff is the set itself plus everything that can be derived from it when only applying strict inference rules (cfr. S. Modgil and H. Prakken, “A general account of argumentation with preferences”, Artificial Intelligence, vol. 195, 2013, p. 361397). Formally: For any 𝑆 ⊆ 𝐿, let the closure of 𝑆 under strict rules, denoted 𝐶𝑙_{𝑅𝑆}(𝑆), be the smallest set containing 𝑆 and the consequent of any strict rule in 𝑅_{𝑆} whose antecedents are in 𝐶𝑙_{𝑅𝑆}. Then the set 𝑆 ⊆ 𝐿 is directly consistent iff ∄ 𝜑, 𝜓 ∈ 𝑆 such that 𝜑 = – 𝜓, and indirectly consistent iff 𝐶𝑙_{𝑅𝑆}(𝑆) is directly consistent.
Whether or not indirect consistency should be assumed and satisfied by ASPIC+ is an issue under debate (cfr. H. Prakken, “Rethinking the Rationality Postulates for ArgumentationBased Inference”, P. Baroni et al. (eds.), Computational Models of Arguments. Proceedings of COMMA 2016, Amsterdam, IOS Press, 2016, p. 419430).
54 ^{ }S. Modgil and H. Prakken, “A general account of argumentation with preferences”, art. cit.
55 ^{ }D. Walton and T.F. Gordon, “Formalizing Informal Logic”, art. cit.
56 ^{ }In a nutshell, the dialectical interaction between the formal and the informal level may be explained through the following shortcut, where 𝙸𝚁 indicates Kreisel’s informal rigour, 𝚂_{1} a specific formal system, 𝚂_{1}^{+} an expansion of it, 𝙿_{𝛴} a set of relevant properties of a formal system 𝛴, and 𝖫_{𝛴} a set of limiting results for 𝛴. The informal rigour process we have been arguing for can thus be described as
… ⇒ 𝙸𝚁 ⇒ 𝚂_{1} ⇒ 𝙿_{𝚂}_{1}, 𝙻_{𝚂}_{1} ⇒ 𝙸𝚁 ⇒ 𝚂_{1}^{+} ⇒ 𝙿_{𝚂}_{1+}, 𝙻_{𝚂}_{1+} ⇒ 𝙸𝚁 ⇒ …
i.e., we have “analysed some intuitive notions and put down their properties”, which corresponds to the first step of 𝙸𝚁; we have thereby obtained 𝚂_{1}; we find out that, with respect to the intuitive notion and their properties, 𝚂_{1}^{+} enjoys some relevant properties 𝙿_{𝛴}, but also suffers from some limiting results 𝖫_{𝛴}; thus, we collect this information and apply 𝙸𝚁 again; we reach an improvement 𝚂_{1}^{+} of 𝚂_{1} (or a collection of them, cfr. N. Barton, Structural relativity and informal rigour, cit.); this will again have relevant properties 𝙿_{𝚂}_{1+} and limits 𝙻_{𝚂}_{1+}; etc.
57 ^{ }G. Crocco, “Informal and absolute proofs…”, art. cit.
Haut de pageTable des illustrations
URL  http://journals.openedition.org/noesis/docannexe/image/6894/img1.png 

Fichier  image/png, 6,9k 
URL  http://journals.openedition.org/noesis/docannexe/image/6894/img2.png 
Fichier  image/png, 15k 
Pour citer cet article
Référence papier
Francesco Montesi et Antonio Piccolomini d’Aragona, « Prawitz’s semantics and Walton’s argument schemes: a tentative reading and application of Kreisel’s informal rigour », Noesis, 38  2022, 1943.
Référence électronique
Francesco Montesi et Antonio Piccolomini d’Aragona, « Prawitz’s semantics and Walton’s argument schemes: a tentative reading and application of Kreisel’s informal rigour », Noesis [En ligne], 38  2022, mis en ligne le 01 juin 2024, consulté le 09 novembre 2024. URL : http://journals.openedition.org/noesis/6894 ; DOI : https://doi.org/10.4000/11xm6
Haut de pageDroits d’auteur
Le texte et les autres éléments (illustrations, fichiers annexes importés), sont « Tous droits réservés », sauf mention contraire.
Haut de page