Bogdan is a philosopher and logician who, for the purposes of this website, acquired the disturbing habit of speaking of himself in the third person.

Currently, Bogdan is a postdoc at the University of Cagliari, where he works in the ALOPHIS research group.

Bogdan moved! As of September 2017, he's a postdoc at the Centre for Philosophy of the University of Lisbon.

As of the 1st of January 2024 Bogdan joined the Philosophy Department of the University of the Witwatersrand in Johannesburg, South Africa.

Before becoming a humble proletarian, Bogdan obtained his PhD from the University of Melbourne with a thesis on logical pluralism written under the supervision of Greg Restall.

What the future will bring, no one knows.

Bogdan is also no longer on twitter and he has an (different) instagram account (than the one) linked here. Bogdan blogs here (although the last post is more than a decade old).

Bogdan is a member of several professional associations, but doesn't keep track of which, with the effect that he rarely pays his dues. He is certain about being a member of Australasian Association for Logic, which, fortunately, does not keep a record of its members and does not charge membership fees. He was never inducted to the Logicians Liberation League, although he is seldom not in the company of several of its members! (He is, however, affiliated with the Deviant Logic Posse.)

Here unfolds the tragedy of Bogdan's Nachgelassene. Each paper lost to the Nachgelassene gets listed here. A click on the titles below will open the abstract of the paper, the publication data and a link to a surprise pdf.

• A proof-theoretic defence of meaning-invariant logical pluralism

  When: 2016

  Where: Mind (125(499):727-757; doi:10.1093/mind/fzv214)

  What about: In this paper I offer a proof-theoretic defence of meaning-invariant logical pluralism. I argue that there is a relation of co-determination between the operational and structural aspects of a logic. As a result, some features of the consequence relation are induced by the connectives. I propose that a connective is defined by those rules which are conservative and unique, while at the same time expressing only connective-induced structural information. This is the key to stabilizing the meaning of the connectives across multiple determinations of the consequence relation.

  Read it here.

• Weak disharmony: some lessons for proof-theoretic semantics

  When: 2016

  Where: The Review of Symbolic Logic (9(3):583-602; doi:10.1017/S1755020316000162)

  What about: A logical constant is weakly disharmonious if its elimination rules are weaker than its introduction rules. Substructural weak disharmony is the weak disharmony generated by structural restrictions on the eliminations. I argue that substructural weak disharmony is not a defect of the constants which exhibit it. To the extent that it is problematic, it calls into question the structural properties of the derivability relation. This prompts us to rethink the issue of controlling the structural properties of a logic by means of harmony. I argue that such a control is possible and desirable. Moreover, it is best achieved by global tests of harmony.

  Read it here.

• On a generality condition in proof-theoretic semantics

  When: 2017

  Where: Theoria, 83(4): 394–418

  What about: Recently, Nissim Francez defended a generality condition on defining rules in proof-theoretic semantics, according to which the schematic formulation of the defining rules must be maximally general. (See his wonderful book, Proof-theoretic semantics.) Context variables must always be present in the schematic rules and they should range over arbitrary collections of formulae. Moreover, no restrictions must be placed on the contexts of these rules. I argue against imposing such a condition.

  Read it here

• ST, LP, and tolerant metainferences (with Francesco Paoli)

  When: 2019

  Where: C. Baskent and T. Ferguson (eds.), Graham Priest on Dialetheism and Paraconsistency, pp. 383--407

  What about: The strict-tolerant (ST) approach to paradox promises to erect theories of naïve truth and tolerant vagueness on the safe bedrock of classical logic. We assess the extent to which this claim is founded. Building on some results by Girard [11], we show that the usual proof-theoretic formulation of propositional ST in terms of the classical sequent calculus without primitive Cut is incomplete with respect to ST-valid metainferences, and exhibit a complete calculus for the same class of metainferences. We also argue that the latter calculus, far from coinciding with classical logic, is a close kin of Priest’s LP.

  Read a drafthere.

• Hopeful monsters: A note on multiple conclusions

  When: 2020

  Where: Erkenntnis, 85: 77–98

  What about: Arguments are usually understood as having one or more premises and only one conclusion. However, this notion of argument can be generalised and we may let arguments have not one, but several disjunctively connected conclusions. This is a contentious generalisation. In this paper I will argue that it is, nonetheless, justified. I argue that multiple conclusions are epiphenomena of the logical connectives. That is, I argue that some connectives induces multiple-conclusion derivations. In this sense, such derivations are completely natural. Moreover, I argue that they can safely be used in the proof-theoretic semantics.

  Read it here.

• Variations on intra-theoretical logical pluralism: Internal vs. external consequence

  When: 2020

  Where: Philosophical Studies, 177: 667–686

  What about: Intra-theoretical logical pluralism is a form of meaning-invariant pluralism about logic, articulated recently by Hjortland (2013). This version of pluralism relies on it being possible to define several distinct notions of provability relative to the same logical calculus. The present paper picks up and explores this theme: How can a single logical calculus express several different consequence relations? The main hypothesis articulated here is that the divide between the internal and external consequence relations in Gentzen systems generates a form of intra-theoretical logical pluralism.

  Read it here.

• The original sin of proof-theoretic semantics (with Francesco Paoli)

  When: 2021

  Where: Synthese, 198: 615–640

  What about: Proof-theoretic semantics is an alternative to model-theoretic seman- tics. It aims at explaining the meaning of the logical constants in terms of the inference rules that govern their behaviour in proofs. We argue that this must be construed as the task of explaining these meanings relative to a logic, i.e., to a consequence relation. Alas, there is no agreed set of properties that a relation must have in order to qualify as a consequence relation. Moreover, the association of a consequence relation to a logical calculus is not as straightforward as it may seem. We show that these facts are problematic for the proof-theoretic project but the problems can be solved. Our thesis is that the consequence relation relevant for proof- theoretic semantics is the one given be the sequent-to-sequent derivability relation in Gentzen systems.

  Read it here.

• Cut for bilateralist intuitionists

  When: 2020

  Where: Analysis, 80: 20--30

  What about: On a bilateralist reading, sequents are interpreted as statements to the effect that, given the assertion of the antecedent it is incoherent to deny the succedent. This interpretation goes against its own ecumenical ambitions, endowing Cut with a meaning very close to that of tertium non datur and thus rendering it intuitionistically unpalatable. This paper explores a top-down route for arguing that, even intuitionistically, a prohibition to deny is as strong as a license to assert. (Note: The official title of the paper is 'Ask not what bilateralist intuitionists can do for Cut, but what Cut can do for bilateralist intuitionism'.)

  Read it here.

• Requiem for logical nihilism, or: Logical nihilism annihilated

  When: 2021

  Where: Synthese, 198(8): 7073–7096

  What about: Logical nihilism is the view that the relation of logical consequence is empty: there are counterexamples to any putative logical law. In this paper, I argue that the nihilist threat is illusory. The nihilistic arguments do not work. Moreover, the entire project is based on a misguided interpretation of the generality of logic.

  Read it here.

• Reflective equilibrium on the fringe

  When: 2022

  Where: Dialectica, 74(2): 247–270

  What about: Reflective equilibrium, as a methodology for the `formation of logics', fails on the fringe, i.e., where intricate details can make or break a logical theory. On the fringe, the process of theorification cannot be methodologically governed by anything like reflective equilibrium. When logical theorising gets tricky, there is nothing on the pre-theoretical side on which our theoretical claims can reflect of -- at least not in any meaningful way. Indeed, the fringe is exclusively the domain of theoretical negotiations and the methodological power of reflective equilibrium is merely nominal. (Note: The full title of the paper is 'Reflective equilibrium on the fringe: The tragic threefold story of a failed methodology for logical theorising'.)

  Read it: here.

• Lógicas subestruturais

  When: 2022

  Where: Compêndio em Linha de Problemas de Filosofia Analítica

  What about: This is a survey article (in Portuguese) presenting the state of the art in the philosophical research on substructural logics. You can read it in Portuguese here. The English version (which may nonetheless contain quite a few typos) is available here.

  Read it at the links above.

• Substructural heresies

  When: 2023

  Where: Inquiry

  What about: This paper discusses two revisionary views about substructurality. The first attempts to reduce the structural features of a logic to properties of its logical vocabulary. It will be found to be untenable. The second aims to separate the structural features of a logic from the properties of logical consequence and to reinterpreted them as sui generis proof resources. I will argue that it is a viable path for a renewed understanding of substructurality.

  Read it: here.

• Logical metainferentialism (with Francesco Paoli)

  When: forthcoming

  Where: Ergo

  What about: Logical inferentialism is the view that the meaning of logical con- stants is implicitly defined by the operational rules that govern their behaviour in proofs – in particular, sequent calculus proofs, according to an increasingly dominant tendency. A tenable articulation of this view presupposes a clarification of certain crucial aspects, concerning e.g. harmony criteria for rules or what counts as a normal proof. Sequent calculus inferentialists generally do so in terms of proofs from axioms, not of derivations from assumptions. Logical metainferentialism calls into question this dogma, against the backdrop of the idea (advocated in The original sin of proof-theoretic semantics (Synthese, 198: 615–640)) that meaning determination is relative to sequent-to-sequent derivability relations of Gentzen systems. We advance a suggestion towards a metainferentially appropriate reformulation of harmony, and explore its potential by focussing on a case study, the calculi for FDE and its extensions.

  Read it: here.

• Metainferential levels and inferential networks (with Francesco Paoli)

  When: forthcoming

  Where: Logique et analyse

  What about: Metainferentialism is the view that a logic is determined by its valid metainferences. It comes in two variants. The finitist version holds that logical consequence is determined by derivability relations between generalised sequents. This is always a Tarskian consequence relation. According to the transfinitist version, one cannot stop here. Instead, all the possible metainferential levels should be taken into consideration when specifying a logic. We defend the finitist version against tranfinitist criticism, clarifying, on the way, the central tenets of finitist metainferentialism. By way of concluding we offer a novel generic interpretation of sequents which breaks with their usual construal as reified inferences.

  Read it: soon!

• Non-foundationalist frameworks for logical metainferentialism

  When: forthcoming

  Where: Synthese

  What about: Standard accounts of logical consequence take it to be determined by valid inferences. Recently, it has been argued that valid inferences underdetermine consequence. Instead, consequence should be characterised as determined by metainferences, i.e., inferences between inferences. For all its benefits, this view faces various problems, including the fact that it appears to be incompatible with the phenomenology of the inferential practice, and the widely endorsed idea that simplicity and naturalness should guide logical theorising. This paper rejects this idea, arguing that, in its extreme form, it amounts to an untenable form of foundationalism about logical consequence. Instead, I will argue that metainferentialism is best embraced and further justified from the standpoint of a broadly constructionist (in the sense of Floridi) approach to logic.

  Read it: soon!

Bogdan is a bit more reluctant when it comes to sharing drafts. So, until he gathers up his courage, here are the tentative titles and abstracts of the draft papers. If you really want them, drop him an email saying so.

• Canonical derivations in Gentzen systems

  Canonical derivations are derivation ending in an application of an introduction rule for the main connective of their conclusion. The notion is as effective as it is simple but recent developments have pointed to the need of extending the standard notion of canonicity in various ways. This paper takes a closer look at different notions of canonicity in Gentzen systems, including sequent calculi extended with elimination rules.

• The Evans counterpoint (with Greg Restall)

  Evans argued that multiple conclusions are disguised disjunctions. In this paper we argue that in a multiple-conclusion argument the conclusions are not all asserted but, at the same time, they are necessarily disjunctions.

• Dual-intuitionistic logic, substructurality, and logical consequence

  This paper analyses dual-intuitionistic logic from a metainferential perspective, i.e., looking at its sequents-to-sequent derivability relation. Some (surprising) results concerning the `substructurality' of its consequence relation are brought to the fore.

• Tolerant conditionals

  In sequent calculi fro classical and intuitionistic logic there are serveral possibilities for formulating introduction and elimination rules for the conditional. These rules can be classified according to the `amount' of Cut they contain. In this paper I investigate the extent to which these rules can serve to codify the behaviour of the conditional in the context of tolerant conseuquence relations which generate radically substructural (= non-reflexive or non-transitive) logics.

• Meaning, rules, and proofs

  This year In 2017, Bogdan taught is teaching a doctoral course on proof-theoretic semantics and some other stuff. (No verbs updated from this point on!) It's fun. He has one formal student, so he feels a bit like Frege. Fortunately, there's no reason for him to feel like Violetta (you know, solo, abbandonato in questo popoloso deserto and so on and so forth). That's because he has a wider audience consisting of other students, colleagues, and supra-colleagues (i.e., the boss, Francesco Paoli). Click here for the syllabus.

• Teaching at Lisbon

  Belonging to the upper classes (=being a postdoc) Bogdan did not have any formal teaching duties and so did not do much teaching in Lisbon. Out of the kindness of his heart, he nevertheless taught a module on Logical consequence in a masters course (in 2018) and in 2023 co-taught, with Bruno Jacinto, a course on the Philosophy of Mathematics.

• Epistemology and metaphysics

  This is an undergraduate course offered in the 2nd term at Wits. It's fun and Bogdan is trying his hand at hybrid teaching. The most metaphysical reading of the course is perhaps Greg Restall's Invention is the mother of necessity.

• Future courses

  In the second semester of 2024, Bogdan will teach a postgraduate course in the Philosophy of language and, in the third term, an undergraduate course on Symbolic logic.

• PSAST=Proof Society Autumn School Tutorial

  Bogdan will teach a Tutorial on Proof-Theoretis Semantics at the 4th International Autumn School on Proof Theory which will take place between the 7th and the 10th November at the University of Utrecht. More information about the event is available here. Click around that page to find more about the Society. For more about the tutorial, keep reading or click here for a pdf version of the text to follow.

  Proof-theoretic semantics (PTS) is an inferentialist theory of meaning which originates in the work of Gentzen in the 1930s and was subsequently devel- oped by Prawitz, Martin-Lof, Dummett, and more recently by Schroeder-Heister, who also baptised the theory, and many others. It is an alternative to Tarskian model-theoretic semantics, aiming to explain the meaning of the logical constants in terms of the rules of inference that govern their behaviour in proofs. The orthodox version of PTS, developed against the background of natural deduction, can be described as an extended attempt to develop Gentzen’s suggestion that ‘the introduction [rules] represent, as it were, the ‘definitions’ of the [logical constants], and the eliminations are no more [...] than the consequences of these definitions’. At its core lies the notion of harmony: a kind of balance between the relative strength of the introductions and eliminations of a logical constant that testifies to their successfully defining a logical constant. The quest for a formal property that accurately captures the intuitive notion of harmony has dominated much of PTS. Said quest is the source of less orthodox versions of PTS. By and large, these retain the focus on harmony, while taking revisionary stances with respect to other aspects of orthodox PTS, such as the priority of the standard assertionist setting of PTS, or of natural deduction. The first part of the tutorial will critically discuss orthodox PTS, focusing on the development of different conceptions of harmony and their con- nection with formal properties of Gentzen-style calculi, such as reducibility, invertibility and normalizability or cut-elimination. The second part of the tutorial is devoted to less orthodox stances in PTS. We will first look at bilateralist versions of the programme, which put denial on a par with assertion and thus introduce a new dimension of harmony, between the conditions for asserting and, respectively, denying a sentence. Finally, we will look at versions of PTS that take the sequent calculus as the framework of choice for specifying definitional rules for the logical connectives. We will explore the motivation(s) for going down this path and some results obtained within this framework.

  We will cover the following topics:

  1. Orthodox PTS

     1. The Gentzenian roots of PTS

        1. Gentzen style calculi

        2. Introductions as definitions; philosophical grounding and harmony

        3. Reducibility and the justification of the eliminations; proof-theoretic validity

     2. Further developments

        1. Prior’s tonk and a different measure of harmony

        2. Conservativeness, normalisability and cut-elimination; the subformula property

        3. Local and global harmony; definitional rules revisited

        4. Weak and strong disharmony; stability

  2. Less orthodox PTS

     1. Bilateralism

        1. Assertion and denial on all fours

        2. Bilateralism in natural deduction; which rules?

        3. Bilateralism in the sequent calculus

     2. The sequent calculus as a basis for PTS

        1. The metatheoretic interpretations of the sequent calculus; sequents as relata of consequence

        2. Harmony and invertibility

        3. Non-transitive and non-reflexive logics; invertibility revisited

  Literature guide

  The classics. The fundamental texts of PTS are (Gentzen 1935; Prawitz 1965) and (dummett91?). Another important historical reference is (Martin-Löf 1996), although this tutorial will not engage much with this strand of PTS.

  Overviews. For a fast paced yet comprehensive survey of many important topics in PTS, see (Schroeder-Heister 2018). (Francez 2015) is the only extant modern monograph on the topic, reporting a wealth of new results mainly in the orthodox tradition, with interesting glimpses into bilateralism as well.

  The texts mentioned in the previous two paragraph just about cover topic (I), particularly if the list of references in (Schroeder-Heister 2018) is used as a resource. An extensive analysis of the extant conceptions of proof-theoretic validity can be found in (Schroeder-Heister 2006).

  Prior’s tonk is introduced in (Prior 1960); PTS (in particular (dummett91?)) draws heavily on the solution to it proposed in (Belnap 1962). For a wider perspective on Belnap’s approach to definitional success, see (Restall 2010). The relation between normalisation and cut-elimination is explored at length in (Ungar 1992). The mysteriously titled topic ‘definitional rules revisited’ has to do with the topics broached in (Prawitz 2007); see also (Queiroz 2008), (Schroeder-Heister 2007b); see also (Bogdan Dicher 2020).

  For topics b ii an iii (local and global harmony) as well as b iv, one can start from (Steinberger 2011) and (Bogdan Dicher 2016). (Read 2010) is important for reviving Gentzen’s idea that the elimination rules are a ‘function’ of the introductions. For the last topic (stability), see also (Jacinto and Read 2017).

  Proof-theoretic bilateralism is by now a well-established field of inquiry. Against the background of natural deduction, it has resurged with particular vigour in (Rumfitt 2000); see also (Francez 2015). For a historically informed wider analysis of bilaterlaism, see (Humberstone 2000). Rumfitt’s proposal is problematic, as shown by (Ferreira 2008) and his solution ((Rumfitt 2008)) less than satisfactory. See also (Valle-Inclan and Schlöder 2022). For sequent-calculus approaches to bilateralism, see (Restall 2005) and also (Bogdan Dicher 2019). For a different take on the same issue, see (Schroeder-Heister 2007a).

  For the topics under 2(b): the so-called metatheoretic interpretation of the sequent calculus is pervasive, albeit mostly understated, throughout the history of PTS. Clear statements of the position can be found in (Hacking 1979; Tennant 2017). A forceful criticism of the view appears in (Schroeder-Heister 2011); see also (Schroeder-Heister 2008). The view that sequent are the proper consequence carrier if further developed in (Bogdan Dicher and Paoli 2021). A tentative theory of harmony appropriate for this new setting is provided in (B. Dicher and Paoli, n.d.).

  Belnap, Nuel D. 1962. “Tonk, Plonk and Plink.” Analysis 22: 130–34.

  Dicher, Bogdan. 2016. “Weak Disharmony: Some Lessons for Proof-Theoretic Semantics.” Review of Symbolic Logic 9 (3): 583–602.

  ———. 2019. “Ask not what bilateralist intuitionists can do for Cut, but what Cut can do for bilateralist intuitionism.” Analysis 80 (1): 30–40. https://doi.org/10.1093/analys/anz023.

  ———. 2020. “Hopeful Monsters: A Note on Multiple Conclusions.” Erkenntnis 85: 77–98. https://doi.org/10.1007/s10670-018-0019-3.

  Dicher, Bogdan, and Francesco Paoli. 2021. “The Original Sin of Proof-Theoretic Semantics.” Synthese 198: 615–40. https://doi.org/10.1007/s11229-018-02048-x.

  Dicher, B., and F. Paoli. n.d. “On Harmony and Metasequents (or: Harmony Without Identity and Cut).”

  Ferreira, Fernando. 2008. “The Co-ordination Principles: A Problem for Bilateralism.” Mind 117 (468): 1051–57. https://doi.org/10.1093/mind/fzn036.

  Francez, Nissim. 2015. Proof-Theoretic Semantics. College Publications.

  Gentzen, Gerhard. 1935. “Untersuchungen über Das Logische Schließen. I,II.” Mathematische Zeitschrift 39 (1): 176-210; 405-431.

  Hacking, Ian. 1979. “What Is Logic?” The Journal of Philosophy 76: 285–319.

  Humberstone, Lloyd. 2000. “The Revival of Rejective Negation.” Journal of Philosophical Logic 29 (4): 331–81.

  Jacinto, Bruno, and Stephen Read. 2017. “General Elimination Stability.” Studia Logica 105: 361–405.

  Martin-Löf, Per. 1996. “On the Meaning of the Logical Constants and the Justification of the Logial Laws.” Nordic Journal of Philosophical Logic 1: 11–69.

  Prawitz, Dag. 1965. Natural Deduction: A Proof Theoretical Study. Stockholm: Almqvist; Wiksell.

  ———. 2007. “Pragmatist and Verificationist Theories of Meaning.” In The Philosophy of Michael Dummett, edited by R. E. Auxier and L. E. Hahn, 455–81. Chicago, La Salle: Open Court.

  Prior, Arthur N. 1960. “The Runabout Inference-Ticket.” Analysis 21 (2): 38–39.

  Queiroz, Ruy de. 2008. “On Reduction Rules, Meaning-as-Use, and Proof-Theoretic Semantics.” Studia Logica.

  Read, Stephen. 2010. “General-Elimination Harmony and the Meaning of the Logical Constants.” Journal of Philosophical Logic 39: 557–76.

  Restall, Greg. 2005. “Multiple Conclusions.” In Logic, Methodology and Philosophy of Science: Proceedings of the Twelfth International Congress, edited by Petr Hájek, Luis Valdés-Villanueva, and Dag Westerståhl, 189–205. KCL Publications. http://www.consequently.org/writing/multipleconclusions/.

  ———. 2010. “Proof Theory and Meaning: On the Context of Deducibility.” In Logic Colloquium 2007, 204–19. Cambridge University Press.

  Rumfitt, Ian. 2000. “‘Yes’ and ‘No’.” Mind 109 (436): 781–823.

  ———. 2008. “Co-ordination Principles: A Reply.” Mind 117 (468): 1059–63. https://doi.org/10.1093/mind/fzn032.

  Schroeder-Heister, Peter. 2006. “Validity Concepts in Proof-Theoretic Semantics.” Synthese 148 (3): 525–71.

  ———. 2007a. “Definitional Reasoning in Proof-Theoretic Semantics and the Square of Opposition.” In The Square of Opposition: A General Framework for Cognition, edited by Jean-Yves Béziau and Gillman Payette, 323–49. Peter Lang.

  ———. 2007b. “Generalized Definitional Reflection and the Inversion Principle.” Logica Universalis 1: 355–76.

  ———. 2008. “Sequent Calculi and Bidirectional Natural Deduction: On the Proper Basis of Proof-Theoretic Semantics.” The Logica Yearbook, 237–51.

  ———. 2011. “The Categorical and the Hypothetical: A Critique of Some Fundamental Assumptions of Standard Semantics.” Synthese 187 (3): 925–42. https://doi.org/10.1007/s11229-011-9910-z.

  ———. 2018. “Proof-Theoretic Semantics.” In The Stanford Encyclopedia of Philosophy, edited by Edward N. Zalta, Spring 2018. https://plato.stanford.edu/archives/spr2018/entries/proof-theoretic-semantics/; Metaphysics Research Lab, Stanford University.

  Steinberger, Florian. 2011. “What Harmony Could and Could Not Be.” Australasian Journal of Philosophy 89: 617–39.

  Tennant, Neil. 2017. Core Logic. Oxford University Press.

  Ungar, A. M. 1992. Normalization, Cut-Elimination, and the Theory of Proofs. Stanford: CSLI Publications.

  Valle-Inclan, Pedro del, and Julian J Schlöder. 2022. “Coordination and Harmony in Bilateral Logic.” Mind, July. https://doi.org/10.1093/mind/fzac012.

How do you feel about the musical version of it? Click here. Well, Bogdan may have exagerated when doctoring it: for one thing, he can't whistle. (Oh, you don't like opera? In that case, you get exclusive access to Bogdan's personal playlist.)

The short version is here.

The technical aspects. This site is made with Hugo and hosted on GitHub - so Bogdan borrowed Rohan's idea of stealing consequently's idea. Using Hugo was quite unnecessary: Bogdan soon realised that he needs to write a theme. For that, he'd have had to understand the syntax of Go. But his procrastination needs are nowhere near so complex. So, he went over to codrops, lawfully appropriated this template, and cheerfully (and mercilessly) hacked the css and html provided. By Paris, you should enjoy the result: the colour scheme of the previous live version was inspired by the rainbow lorikeet.

The grand perspective. It's grand but simple and elaborated by John Perry. Bogdan had bucketloads of work to do, so he decided to revive his website.